consider D1, D2, D3, D4, D5, D6, D7, D8 being Element of 6 -tuples_on BOOLEAN such that
L0: ( 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 thDESDIV8;
consider x1 being Element of 4 -tuples_on BOOLEAN such that
L1: x1 = N16toB4 . (DES-SBOX1 . (B6toN64 D1)) ;
consider x2 being Element of 4 -tuples_on BOOLEAN such that
L2: x2 = N16toB4 . (DES-SBOX2 . (B6toN64 D2)) ;
consider x3 being Element of 4 -tuples_on BOOLEAN such that
L3: x3 = N16toB4 . (DES-SBOX3 . (B6toN64 D3)) ;
consider x4 being Element of 4 -tuples_on BOOLEAN such that
L4: x4 = N16toB4 . (DES-SBOX4 . (B6toN64 D4)) ;
consider x5 being Element of 4 -tuples_on BOOLEAN such that
L5: x5 = N16toB4 . (DES-SBOX5 . (B6toN64 D5)) ;
consider x6 being Element of 4 -tuples_on BOOLEAN such that
L6: x6 = N16toB4 . (DES-SBOX6 . (B6toN64 D6)) ;
consider x7 being Element of 4 -tuples_on BOOLEAN such that
L7: x7 = N16toB4 . (DES-SBOX7 . (B6toN64 D7)) ;
consider x8 being Element of 4 -tuples_on BOOLEAN such that
L8: x8 = N16toB4 . (DES-SBOX8 . (B6toN64 D8)) ;
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
LFF: FIT = ((((((x1 ^ x2) ^ x3) ^ x4) ^ x5) ^ x6) ^ x7) ^ x8 ;
reconsider PFIT = DES-P FIT as Element of 32 -tuples_on BOOLEAN ;
take PFIT ; :: thesis: 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 L0, L1, L2, L3, L4, L5, L6, L7, L8, LFF; :: thesis: verum