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