:: deftheorem defines bitshift_DES DESCIP_1:def 27 :
for b₁ being FinSequence of NAT holds
( b₁ = bitshift_DES iff ( b₁ is 16 -element & b₁ . 1 = 1 & b₁ . 2 = 1 & b₁ . 3 = 2 & b₁ . 4 = 2 & b₁ . 5 = 2 & b₁ . 6 = 2 & b₁ . 7 = 2 & b₁ . 8 = 2 & b₁ . 9 = 1 & b₁ . 10 = 2 & b₁ . 11 = 2 & b₁ . 12 = 2 & b₁ . 13 = 2 & b₁ . 14 = 2 & b₁ . 15 = 2 & b₁ . 16 = 1 ) );