:: deftheorem defines DES-SBOX8 DESCIP_1:def 13 :
for b₁ being Function of 64,16 holds
( b₁ = DES-SBOX8 iff ( b₁ . 0 = 13 & b₁ . 1 = 2 & b₁ . 2 = 8 & b₁ . 3 = 4 & b₁ . 4 = 6 & b₁ . 5 = 15 & b₁ . 6 = 11 & b₁ . 7 = 1 & b₁ . 8 = 10 & b₁ . 9 = 9 & b₁ . 10 = 3 & b₁ . 11 = 14 & b₁ . 12 = 5 & b₁ . 13 = 0 & b₁ . 14 = 12 & b₁ . 15 = 7 & b₁ . 16 = 1 & b₁ . 17 = 15 & b₁ . 18 = 13 & b₁ . 19 = 8 & b₁ . 20 = 10 & b₁ . 21 = 3 & b₁ . 22 = 7 & b₁ . 23 = 4 & b₁ . 24 = 12 & b₁ . 25 = 5 & b₁ . 26 = 5 & b₁ . 27 = 11 & b₁ . 28 = 0 & b₁ . 29 = 14 & b₁ . 30 = 9 & b₁ . 31 = 2 & b₁ . 32 = 7 & b₁ . 33 = 11 & b₁ . 34 = 4 & b₁ . 35 = 1 & b₁ . 36 = 9 & b₁ . 37 = 12 & b₁ . 38 = 14 & b₁ . 39 = 2 & b₁ . 40 = 0 & b₁ . 41 = 6 & b₁ . 42 = 10 & b₁ . 43 = 13 & b₁ . 44 = 15 & b₁ . 45 = 3 & b₁ . 46 = 5 & b₁ . 47 = 8 & b₁ . 48 = 2 & b₁ . 49 = 1 & b₁ . 50 = 14 & b₁ . 51 = 7 & b₁ . 52 = 4 & b₁ . 53 = 10 & b₁ . 54 = 8 & b₁ . 55 = 13 & b₁ . 56 = 15 & b₁ . 57 = 12 & b₁ . 58 = 9 & b₁ . 59 = 0 & b₁ . 60 = 3 & b₁ . 61 = 5 & b₁ . 62 = 6 & b₁ . 63 = 11 ) );