:: deftheorem defines DES-F DESCIP_1:def 23 :
for R being Element of 32 -tuples_on BOOLEAN
for RKey being Element of 48 -tuples_on BOOLEAN
for b₃ being Element of 32 -tuples_on BOOLEAN holds
( b₃ = DES-F (R,RKey) iff ex D1, D2, D3, D4, D5, D6, D7, D8 being Element of 6 -tuples_on BOOLEAN ex x1, x2, x3, x4, x5, x6, x7, x8 being Element of 4 -tuples_on BOOLEAN ex C32 being Element of 32 -tuples_on BOOLEAN st
( D1 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 1 & D2 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 2 & D3 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 3 & D4 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 4 & D5 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 5 & D6 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 6 & D7 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 7 & D8 = (DES-DIV8 (Op-XOR ((DES-E R),RKey))) . 8 & Op-XOR ((DES-E R),RKey) = ((((((D1 ^ D2) ^ D3) ^ D4) ^ D5) ^ D6) ^ D7) ^ D8 & x1 = N16toB4 (DES-SBOX1 . (B6toN64 D1)) & x2 = N16toB4 (DES-SBOX2 . (B6toN64 D2)) & x3 = N16toB4 (DES-SBOX3 . (B6toN64 D3)) & x4 = N16toB4 (DES-SBOX4 . (B6toN64 D4)) & x5 = N16toB4 (DES-SBOX5 . (B6toN64 D5)) & x6 = N16toB4 (DES-SBOX6 . (B6toN64 D6)) & x7 = N16toB4 (DES-SBOX7 . (B6toN64 D7)) & x8 = N16toB4 (DES-SBOX8 . (B6toN64 D8)) & C32 = ((((((x1 ^ x2) ^ x3) ^ x4) ^ x5) ^ x6) ^ x7) ^ x8 & b₃ = DES-P C32 ) );