:: deftheorem defines DES-E DESCIP_1:def 18 :
for r being Element of 32 -tuples_on BOOLEAN
for b₂ being Element of 48 -tuples_on BOOLEAN holds
( b₂ = DES-E r iff ( b₂ . 1 = r . 32 & b₂ . 2 = r . 1 & b₂ . 3 = r . 2 & b₂ . 4 = r . 3 & b₂ . 5 = r . 4 & b₂ . 6 = r . 5 & b₂ . 7 = r . 4 & b₂ . 8 = r . 5 & b₂ . 9 = r . 6 & b₂ . 10 = r . 7 & b₂ . 11 = r . 8 & b₂ . 12 = r . 9 & b₂ . 13 = r . 8 & b₂ . 14 = r . 9 & b₂ . 15 = r . 10 & b₂ . 16 = r . 11 & b₂ . 17 = r . 12 & b₂ . 18 = r . 13 & b₂ . 19 = r . 12 & b₂ . 20 = r . 13 & b₂ . 21 = r . 14 & b₂ . 22 = r . 15 & b₂ . 23 = r . 16 & b₂ . 24 = r . 17 & b₂ . 25 = r . 16 & b₂ . 26 = r . 17 & b₂ . 27 = r . 18 & b₂ . 28 = r . 19 & b₂ . 29 = r . 20 & b₂ . 30 = r . 21 & b₂ . 31 = r . 20 & b₂ . 32 = r . 21 & b₂ . 33 = r . 22 & b₂ . 34 = r . 23 & b₂ . 35 = r . 24 & b₂ . 36 = r . 25 & b₂ . 37 = r . 24 & b₂ . 38 = r . 25 & b₂ . 39 = r . 26 & b₂ . 40 = r . 27 & b₂ . 41 = r . 28 & b₂ . 42 = r . 29 & b₂ . 43 = r . 28 & b₂ . 44 = r . 29 & b₂ . 45 = r . 30 & b₂ . 46 = r . 31 & b₂ . 47 = r . 32 & b₂ . 48 = r . 1 ) );