:: deftheorem DefInvShiftRows defines InvShiftRows AESCIP_1:def 5 :
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))) holds
( b₁ = InvShiftRows iff for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (b₁ . input) . i = Op-Shift (xi,(i - 1)) ) );