consider D1, D2, D3, D4, D5, D6, D7, D8 being Element of 6 -tuples_on BOOLEAN such that
A1:
( 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 )
by Th29;
reconsider x1 = N16toB4 (DES-SBOX1 . (B6toN64 D1)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x2 = N16toB4 (DES-SBOX2 . (B6toN64 D2)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x3 = N16toB4 (DES-SBOX3 . (B6toN64 D3)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x4 = N16toB4 (DES-SBOX4 . (B6toN64 D4)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x5 = N16toB4 (DES-SBOX5 . (B6toN64 D5)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x6 = N16toB4 (DES-SBOX6 . (B6toN64 D6)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x7 = N16toB4 (DES-SBOX7 . (B6toN64 D7)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x8 = N16toB4 (DES-SBOX8 . (B6toN64 D8)) as Element of 4 -tuples_on BOOLEAN by FINSEQ_2:131;
len (((((((x1 ^ x2) ^ x3) ^ x4) ^ x5) ^ x6) ^ x7) ^ x8) = 32
by CARD_1:def 7;
then
((((((x1 ^ x2) ^ x3) ^ x4) ^ x5) ^ x6) ^ x7) ^ x8 is Element of 32 -tuples_on BOOLEAN
by FINSEQ_2:92;
then consider FIT being Element of 32 -tuples_on BOOLEAN such that
A2:
FIT = ((((((x1 ^ x2) ^ x3) ^ x4) ^ x5) ^ x6) ^ x7) ^ x8
;
reconsider PFIT = DES-P FIT as Element of 32 -tuples_on BOOLEAN ;
take
PFIT
; 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 & PFIT = DES-P C32 )
thus
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 & PFIT = DES-P C32 )
by A1, A2; verum