:: Formalization of the Data Encryption Standard
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 30, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users

registration

let n be Nat;
let f be n -element FinSequence;

cluster Rev f -> n -element ;

coherence
Rev f is n -element

proof end;

end;

definition

let D be non empty set ;
let n be Nat;
let f be Element of n -tuples_on D;
:: original: Rev
redefine func Rev f -> Element of n -tuples_on D;
coherence
Rev f is Element of n -tuples_on D

proof end;

end;

notation

let n be Nat;
let f be FinSequence;
synonym Op-Left (f,n) for f | n;
synonym Op-Right (f,n) for f /^ n;

end;

definition

let D be non empty set ;
let n be Nat;
let f be FinSequence of D;
:: original: Op-Left
redefine func Op-Left (f,n) -> FinSequence of D;
coherence
Op-Left (f,n) is FinSequence of D

proof end;

:: original: Op-Right
redefine func Op-Right (f,n) -> FinSequence of D;
coherence
Op-Right (f,n) is FinSequence of D

proof end;

end;

notation

let D be non empty set ;
let n be Nat;
let s be Element of (2 * n) -tuples_on D;
synonym SP-Left s for Op-Left (n,D);
synonym SP-Right s for Op-Right (n,D);

end;

definition

let D be non empty set ;
let n be Nat;
let s be Element of (2 * n) -tuples_on D;
:: original: Op-Left
redefine func SP-Left s -> Element of n -tuples_on D;
coherence
Op-Left (s,n) is Element of n -tuples_on D

proof end;

end;

theorem Th1: :: DESCIP_1:1

for D being non empty set
for m, n being non zero Element of NAT
for s being Element of n -tuples_on D st m <= n holds
Op-Left (s,m) is Element of m -tuples_on D

proof end;

theorem Th2: :: DESCIP_1:2

for D being non empty set
for m, n, l being non zero Element of NAT
for s being Element of n -tuples_on D st m <= n & l = n - m holds
Op-Right (s,m) is Element of l -tuples_on D

proof end;

definition

let D be non empty set ;
let n be non zero Element of NAT ;
let s be Element of (2 * n) -tuples_on D;
:: original: Op-Right
redefine func SP-Right s -> Element of n -tuples_on D;
coherence
Op-Right (s,n) is Element of n -tuples_on D

proof end;

end;

theorem Th3: :: DESCIP_1:3

for D being non empty set
for n being non zero Element of NAT
for s being Element of (2 * n) -tuples_on D holds (SP-Left s) ^ (SP-Right s) = s by RFINSEQ:8;

definition

let s be FinSequence;

func Op-LeftShift s -> FinSequence equals :: DESCIP_1:def 1
(s /^ 1) ^ <*(s . 1)*>;

coherence
(s /^ 1) ^ <*(s . 1)*> is FinSequence ;

end;

:: deftheorem defines Op-LeftShift DESCIP_1:def 1 :
for s being FinSequence holds Op-LeftShift s = (s /^ 1) ^ <*(s . 1)*>;

theorem Th4: :: DESCIP_1:4

for s being FinSequence st 1 <= len s holds
len (Op-LeftShift s) = len s

proof end;

theorem Th5: :: DESCIP_1:5

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s )

proof end;

theorem :: DESCIP_1:6

for D being non empty set
for n being non zero Element of NAT
for s being Element of n -tuples_on D holds Op-LeftShift s is Element of n -tuples_on D

proof end;

definition

let s be FinSequence;

func Op-RightShift s -> FinSequence equals :: DESCIP_1:def 2
(<*(s . (len s))*> ^ s) | (len s);

coherence
(<*(s . (len s))*> ^ s) | (len s) is FinSequence ;

end;

:: deftheorem defines Op-RightShift DESCIP_1:def 2 :
for s being FinSequence holds Op-RightShift s = (<*(s . (len s))*> ^ s) | (len s);

theorem Th7: :: DESCIP_1:7

for s being FinSequence holds len (Op-RightShift s) = len s

proof end;

theorem Th8: :: DESCIP_1:8

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-RightShift s is FinSequence of D

proof end;

theorem :: DESCIP_1:9

for D being non empty set
for n being non zero Element of NAT
for s being Element of n -tuples_on D holds Op-RightShift s is Element of n -tuples_on D

proof end;

definition

let D be non empty set ;
let s be FinSequence of D;
let n be Integer;
assume A1: 1 <= len s ;

func Op-Shift (s,n) -> FinSequence of D means :Def3: :: DESCIP_1:def 3
( len it = len s & ( for i being Nat st i in Seg (len s) holds
it . i = s . ((((i - 1) + n) mod (len s)) + 1) ) );

existence
ex b₁ being FinSequence of D st
( len b₁ = len s & ( for i being Nat st i in Seg (len s) holds
b₁ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of D st len b₁ = len s & ( for i being Nat st i in Seg (len s) holds
b₁ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) & len b₂ = len s & ( for i being Nat st i in Seg (len s) holds
b₂ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Op-Shift DESCIP_1:def 3 :
for D being non empty set
for s being FinSequence of D
for n being Integer st 1 <= len s holds
for b₄ being FinSequence of D holds
( b₄ = Op-Shift (s,n) iff ( len b₄ = len s & ( for i being Nat st i in Seg (len s) holds
b₄ . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) );

theorem :: DESCIP_1:10

for D being non empty set
for s being FinSequence of D
for n, m being Integer st 1 <= len s holds
Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m))

proof end;

theorem :: DESCIP_1:11

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,0) = s

proof end;

theorem :: DESCIP_1:12

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(len s)) = s

proof end;

theorem :: DESCIP_1:13

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(- (len s))) = s

proof end;

theorem Th14: :: DESCIP_1:14

for D being non empty set
for n being non zero Element of NAT
for m being Integer
for s being Element of n -tuples_on D holds Op-Shift (s,m) is Element of n -tuples_on D

proof end;

theorem :: DESCIP_1:15

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(- 1)) = Op-RightShift s

proof end;

theorem :: DESCIP_1:16

for D being non empty set
for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,1) = Op-LeftShift s

proof end;

definition

let x, y be Element of 28 -tuples_on BOOLEAN;
:: original: ^
redefine func x ^ y -> Element of 56 -tuples_on BOOLEAN;
coherence
x ^ y is Element of 56 -tuples_on BOOLEAN

proof end;

end;

definition

let n be non zero Element of NAT ;
let s be Element of n -tuples_on BOOLEAN;
let i be Nat;
:: original: .
redefine func s . i -> Element of BOOLEAN ;
coherence
s . i is Element of BOOLEAN

proof end;

end;

registration

let n be Nat;

cluster -> boolean-valued for Element of n -tuples_on BOOLEAN;

coherence
for b₁ being Element of n -tuples_on BOOLEAN holds b₁ is boolean-valued

proof end;

end;

notation

let n be Element of NAT ;
let s, t be Element of n -tuples_on BOOLEAN;
synonym Op-XOR (s,t) for n 'xor' s;

end;

definition

let n be non zero Element of NAT ;
let s, t be Element of n -tuples_on BOOLEAN;

:: original: Op-XOR
redefine func Op-XOR (s,t) -> Element of n -tuples_on BOOLEAN means :Def4: :: DESCIP_1:def 4
for i being Nat st i in Seg n holds
it . i = (s . i) 'xor' (t . i);

coherence
Op-XOR (t,) is Element of n -tuples_on BOOLEAN

proof end;

compatibility
for b₁ being Element of n -tuples_on BOOLEAN holds
( b₁ = Op-XOR (t,) iff for i being Nat st i in Seg n holds
b₁ . i = (s . i) 'xor' (t . i) )

proof end;

end;

:: deftheorem Def4 defines Op-XOR DESCIP_1:def 4 :
for n being non zero Element of NAT
for s, t, b₄ being Element of n -tuples_on BOOLEAN holds
( b₄ = Op-XOR (s,t) iff for i being Nat st i in Seg n holds
b₄ . i = (s . i) 'xor' (t . i) );

definition

let n, k be non zero Element of NAT ;
let RK be Element of k -tuples_on (n -tuples_on BOOLEAN);
let i be Element of Seg k;
:: original: .
redefine func RK . i -> Element of n -tuples_on BOOLEAN;
coherence
RK . i is Element of n -tuples_on BOOLEAN

proof end;

end;

theorem Th17: :: DESCIP_1:17

for n being non zero Element of NAT
for s, t being Element of n -tuples_on BOOLEAN holds Op-XOR ((Op-XOR (s,t)),t) = s

proof end;

definition

let m be non zero Element of NAT ;
let D be non empty set ;
let L be sequence of (m -tuples_on D);
let i be Nat;
:: original: .
redefine func L . i -> Element of m -tuples_on D;
coherence
L . i is Element of m -tuples_on D

proof end;

end;

definition

let f be Function of 64,16;
let i be set ;
:: original: .
redefine func f . i -> Element of 16;
coherence
f . i is Element of 16

proof end;

end;

theorem Th18: :: DESCIP_1:18

for D being non empty set
for s being FinSequence of D
for n, m being Nat st n + m <= len s holds
(s | n) ^ ((s /^ n) | m) = s | (n + m)

proof end;

scheme :: DESCIP_1:sch 1
QuadChoiceRec{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅() -> Element of F₁(), F₆() -> Element of F₂(), F₇() -> Element of F₃(), F₈() -> Element of F₄(), P₁[ object , object , object , object , object , object , object , object , object ] } :

ex f being sequence of F₁() ex g being sequence of F₂() ex h being sequence of F₃() ex i being sequence of F₄() st
( f . 0 = F₅() & g . 0 = F₆() & h . 0 = F₇() & i . 0 = F₈() & ( for n being Element of NAT holds P₁[n,f . n,g . n,h . n,i . n,f . (n + 1),g . (n + 1),h . (n + 1),i . (n + 1)] ) )

provided

A1: for n being Element of NAT
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for w being Element of F₄() ex x1 being Element of F₁() ex y1 being Element of F₂() ex z1 being Element of F₃() ex w1 being Element of F₄() st P₁[n,x,y,z,w,x1,y1,z1,w1]

proof end;

theorem :: DESCIP_1:19

for n being non zero Nat holds n = {0} \/ ((Seg n) \ {n})

proof end;

theorem Th20: :: DESCIP_1:20

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8 being Element of S ex s being FinSequence of S st
( s is 8 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 )

proof end;

theorem Th21: :: DESCIP_1:21

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16 being Element of S ex s being FinSequence of S st
( s is 16 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 & s . 9 = x9 & s . 10 = x10 & s . 11 = x11 & s . 12 = x12 & s . 13 = x13 & s . 14 = x14 & s . 15 = x15 & s . 16 = x16 )

proof end;

theorem Th22: :: DESCIP_1:22

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32 being Element of S ex s being FinSequence of S st
( s is 32 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 & s . 9 = x9 & s . 10 = x10 & s . 11 = x11 & s . 12 = x12 & s . 13 = x13 & s . 14 = x14 & s . 15 = x15 & s . 16 = x16 & s . 17 = x17 & s . 18 = x18 & s . 19 = x19 & s . 20 = x20 & s . 21 = x21 & s . 22 = x22 & s . 23 = x23 & s . 24 = x24 & s . 25 = x25 & s . 26 = x26 & s . 27 = x27 & s . 28 = x28 & s . 29 = x29 & s . 30 = x30 & s . 31 = x31 & s . 32 = x32 )

proof end;

theorem Th23: :: DESCIP_1:23

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48 being Element of S ex s being FinSequence of S st
( s is 48 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 & s . 9 = x9 & s . 10 = x10 & s . 11 = x11 & s . 12 = x12 & s . 13 = x13 & s . 14 = x14 & s . 15 = x15 & s . 16 = x16 & s . 17 = x17 & s . 18 = x18 & s . 19 = x19 & s . 20 = x20 & s . 21 = x21 & s . 22 = x22 & s . 23 = x23 & s . 24 = x24 & s . 25 = x25 & s . 26 = x26 & s . 27 = x27 & s . 28 = x28 & s . 29 = x29 & s . 30 = x30 & s . 31 = x31 & s . 32 = x32 & s . 33 = x33 & s . 34 = x34 & s . 35 = x35 & s . 36 = x36 & s . 37 = x37 & s . 38 = x38 & s . 39 = x39 & s . 40 = x40 & s . 41 = x41 & s . 42 = x42 & s . 43 = x43 & s . 44 = x44 & s . 45 = x45 & s . 46 = x46 & s . 47 = x47 & s . 48 = x48 )

proof end;

theorem Th24: :: DESCIP_1:24

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56 being Element of S ex s being FinSequence of S st
( s is 56 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 & s . 9 = x9 & s . 10 = x10 & s . 11 = x11 & s . 12 = x12 & s . 13 = x13 & s . 14 = x14 & s . 15 = x15 & s . 16 = x16 & s . 17 = x17 & s . 18 = x18 & s . 19 = x19 & s . 20 = x20 & s . 21 = x21 & s . 22 = x22 & s . 23 = x23 & s . 24 = x24 & s . 25 = x25 & s . 26 = x26 & s . 27 = x27 & s . 28 = x28 & s . 29 = x29 & s . 30 = x30 & s . 31 = x31 & s . 32 = x32 & s . 33 = x33 & s . 34 = x34 & s . 35 = x35 & s . 36 = x36 & s . 37 = x37 & s . 38 = x38 & s . 39 = x39 & s . 40 = x40 & s . 41 = x41 & s . 42 = x42 & s . 43 = x43 & s . 44 = x44 & s . 45 = x45 & s . 46 = x46 & s . 47 = x47 & s . 48 = x48 & s . 49 = x49 & s . 50 = x50 & s . 51 = x51 & s . 52 = x52 & s . 53 = x53 & s . 54 = x54 & s . 55 = x55 & s . 56 = x56 )

proof end;

theorem Th25: :: DESCIP_1:25

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of S ex s being FinSequence of S st
( s is 64 -element & s . 1 = x1 & s . 2 = x2 & s . 3 = x3 & s . 4 = x4 & s . 5 = x5 & s . 6 = x6 & s . 7 = x7 & s . 8 = x8 & s . 9 = x9 & s . 10 = x10 & s . 11 = x11 & s . 12 = x12 & s . 13 = x13 & s . 14 = x14 & s . 15 = x15 & s . 16 = x16 & s . 17 = x17 & s . 18 = x18 & s . 19 = x19 & s . 20 = x20 & s . 21 = x21 & s . 22 = x22 & s . 23 = x23 & s . 24 = x24 & s . 25 = x25 & s . 26 = x26 & s . 27 = x27 & s . 28 = x28 & s . 29 = x29 & s . 30 = x30 & s . 31 = x31 & s . 32 = x32 & s . 33 = x33 & s . 34 = x34 & s . 35 = x35 & s . 36 = x36 & s . 37 = x37 & s . 38 = x38 & s . 39 = x39 & s . 40 = x40 & s . 41 = x41 & s . 42 = x42 & s . 43 = x43 & s . 44 = x44 & s . 45 = x45 & s . 46 = x46 & s . 47 = x47 & s . 48 = x48 & s . 49 = x49 & s . 50 = x50 & s . 51 = x51 & s . 52 = x52 & s . 53 = x53 & s . 54 = x54 & s . 55 = x55 & s . 56 = x56 & s . 57 = x57 & s . 58 = x58 & s . 59 = x59 & s . 60 = x60 & s . 61 = x61 & s . 62 = x62 & s . 63 = x63 & s . 64 = x64 )

proof end;

notation

let n be non zero Nat;
let i be Element of Segm n;
synonym ntoSeg i for succ n;

end;

definition

let n be non zero Nat;
let i be Element of Segm n;
:: original: ntoSeg
redefine func ntoSeg i -> Element of Seg n;
coherence
ntoSeg is Element of Seg n

proof end;

end;

definition

let n be non zero Nat;
let f be Function of (Segm n),(Seg n);

attr f is NtoSEG means :Def5: :: DESCIP_1:def 5
for i being Element of Segm n holds f . i = ntoSeg i;

end;

:: deftheorem Def5 defines NtoSEG DESCIP_1:def 5 :
for n being non zero Nat
for f being Function of (Segm n),(Seg n) holds
( f is NtoSEG iff for i being Element of Segm n holds f . i = ntoSeg i );

registration

let n be non zero Nat;

cluster V1() V4( Segm n) V5( Seg n) Function-like non empty total quasi_total V49() V50() V51() V52() NtoSEG for Element of bool [:(Segm n),(Seg n):];

existence
ex b₁ being Function of (Segm n),(Seg n) st b₁ is NtoSEG

proof end;

end;

Lm1: for n being non zero Nat
for f being NtoSEG Function of (Segm n),(Seg n) holds rng f = Seg n

proof end;

registration

let n be non zero Nat;

cluster Function-like quasi_total NtoSEG -> bijective NtoSEG for Element of bool [:(Segm n),(Seg n):];

coherence
for b₁ being NtoSEG Function of (Segm n),(Seg n) holds b₁ is bijective

proof end;

end;

theorem Th26: :: DESCIP_1:26

for n being non zero Nat
for f being NtoSEG Function of (Segm n),(Seg n)
for i being Nat st i < n holds
( f . i = i + 1 & i in dom f )

proof end;

Lm2: for f being NtoSEG Function of (Segm 64),(Seg 64)
for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of S
for t being Element of 64 -tuples_on S st t . 1 = x1 & t . 2 = x2 & t . 3 = x3 & t . 4 = x4 & t . 5 = x5 & t . 6 = x6 & t . 7 = x7 & t . 8 = x8 & t . 9 = x9 & t . 10 = x10 & t . 11 = x11 & t . 12 = x12 & t . 13 = x13 & t . 14 = x14 & t . 15 = x15 & t . 16 = x16 & t . 17 = x17 & t . 18 = x18 & t . 19 = x19 & t . 20 = x20 & t . 21 = x21 & t . 22 = x22 & t . 23 = x23 & t . 24 = x24 & t . 25 = x25 & t . 26 = x26 & t . 27 = x27 & t . 28 = x28 & t . 29 = x29 & t . 30 = x30 & t . 31 = x31 & t . 32 = x32 & t . 33 = x33 & t . 34 = x34 & t . 35 = x35 & t . 36 = x36 & t . 37 = x37 & t . 38 = x38 & t . 39 = x39 & t . 40 = x40 & t . 41 = x41 & t . 42 = x42 & t . 43 = x43 & t . 44 = x44 & t . 45 = x45 & t . 46 = x46 & t . 47 = x47 & t . 48 = x48 & t . 49 = x49 & t . 50 = x50 & t . 51 = x51 & t . 52 = x52 & t . 53 = x53 & t . 54 = x54 & t . 55 = x55 & t . 56 = x56 & t . 57 = x57 & t . 58 = x58 & t . 59 = x59 & t . 60 = x60 & t . 61 = x61 & t . 62 = x62 & t . 63 = x63 & t . 64 = x64 holds
( (t * f) . 0 = x1 & (t * f) . 1 = x2 & (t * f) . 2 = x3 & (t * f) . 3 = x4 & (t * f) . 4 = x5 & (t * f) . 5 = x6 & (t * f) . 6 = x7 & (t * f) . 7 = x8 & (t * f) . 8 = x9 & (t * f) . 9 = x10 & (t * f) . 10 = x11 & (t * f) . 11 = x12 & (t * f) . 12 = x13 & (t * f) . 13 = x14 & (t * f) . 14 = x15 & (t * f) . 15 = x16 & (t * f) . 16 = x17 & (t * f) . 17 = x18 & (t * f) . 18 = x19 & (t * f) . 19 = x20 & (t * f) . 20 = x21 & (t * f) . 21 = x22 & (t * f) . 22 = x23 & (t * f) . 23 = x24 & (t * f) . 24 = x25 & (t * f) . 25 = x26 & (t * f) . 26 = x27 & (t * f) . 27 = x28 & (t * f) . 28 = x29 & (t * f) . 29 = x30 & (t * f) . 30 = x31 & (t * f) . 31 = x32 & (t * f) . 32 = x33 & (t * f) . 33 = x34 & (t * f) . 34 = x35 & (t * f) . 35 = x36 & (t * f) . 36 = x37 & (t * f) . 37 = x38 & (t * f) . 38 = x39 & (t * f) . 39 = x40 & (t * f) . 40 = x41 & (t * f) . 41 = x42 & (t * f) . 42 = x43 & (t * f) . 43 = x44 & (t * f) . 44 = x45 & (t * f) . 45 = x46 & (t * f) . 46 = x47 & (t * f) . 47 = x48 & (t * f) . 48 = x49 & (t * f) . 49 = x50 & (t * f) . 50 = x51 & (t * f) . 51 = x52 & (t * f) . 52 = x53 & (t * f) . 53 = x54 & (t * f) . 54 = x55 & (t * f) . 55 = x56 & (t * f) . 56 = x57 & (t * f) . 57 = x58 & (t * f) . 58 = x59 & (t * f) . 59 = x60 & (t * f) . 60 = x61 & (t * f) . 61 = x62 & (t * f) . 62 = x63 & (t * f) . 63 = x64 )

proof end;

theorem Th27: :: DESCIP_1:27

for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of S ex f being Function of 64,S st
( f . 0 = x1 & f . 1 = x2 & f . 2 = x3 & f . 3 = x4 & f . 4 = x5 & f . 5 = x6 & f . 6 = x7 & f . 7 = x8 & f . 8 = x9 & f . 9 = x10 & f . 10 = x11 & f . 11 = x12 & f . 12 = x13 & f . 13 = x14 & f . 14 = x15 & f . 15 = x16 & f . 16 = x17 & f . 17 = x18 & f . 18 = x19 & f . 19 = x20 & f . 20 = x21 & f . 21 = x22 & f . 22 = x23 & f . 23 = x24 & f . 24 = x25 & f . 25 = x26 & f . 26 = x27 & f . 27 = x28 & f . 28 = x29 & f . 29 = x30 & f . 30 = x31 & f . 31 = x32 & f . 32 = x33 & f . 33 = x34 & f . 34 = x35 & f . 35 = x36 & f . 36 = x37 & f . 37 = x38 & f . 38 = x39 & f . 39 = x40 & f . 40 = x41 & f . 41 = x42 & f . 42 = x43 & f . 43 = x44 & f . 44 = x45 & f . 45 = x46 & f . 46 = x47 & f . 47 = x48 & f . 48 = x49 & f . 49 = x50 & f . 50 = x51 & f . 51 = x52 & f . 52 = x53 & f . 53 = x54 & f . 54 = x55 & f . 55 = x56 & f . 56 = x57 & f . 57 = x58 & f . 58 = x59 & f . 59 = x60 & f . 60 = x61 & f . 61 = x62 & f . 62 = x63 & f . 63 = x64 )

proof end;

Lm3: 0 is Element of Segm 16 & ... & 15 is Element of Segm 16
by NAT_1:44;

Lm4: for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of 16
for f, g being Function of 64,16 st f . 1 = x1 & f . 2 = x2 & f . 3 = x3 & f . 4 = x4 & f . 5 = x5 & f . 6 = x6 & f . 7 = x7 & f . 8 = x8 & f . 9 = x9 & f . 10 = x10 & f . 11 = x11 & f . 12 = x12 & f . 13 = x13 & f . 14 = x14 & f . 15 = x15 & f . 16 = x16 & f . 17 = x17 & f . 18 = x18 & f . 19 = x19 & f . 20 = x20 & f . 21 = x21 & f . 22 = x22 & f . 23 = x23 & f . 24 = x24 & f . 25 = x25 & f . 26 = x26 & f . 27 = x27 & f . 28 = x28 & f . 29 = x29 & f . 30 = x30 & f . 31 = x31 & f . 32 = x32 & f . 33 = x33 & f . 34 = x34 & f . 35 = x35 & f . 36 = x36 & f . 37 = x37 & f . 38 = x38 & f . 39 = x39 & f . 40 = x40 & f . 41 = x41 & f . 42 = x42 & f . 43 = x43 & f . 44 = x44 & f . 45 = x45 & f . 46 = x46 & f . 47 = x47 & f . 48 = x48 & f . 49 = x49 & f . 50 = x50 & f . 51 = x51 & f . 52 = x52 & f . 53 = x53 & f . 54 = x54 & f . 55 = x55 & f . 56 = x56 & f . 57 = x57 & f . 58 = x58 & f . 59 = x59 & f . 60 = x60 & f . 61 = x61 & f . 62 = x62 & f . 63 = x63 & f . 0 = x64 & g . 1 = x1 & g . 2 = x2 & g . 3 = x3 & g . 4 = x4 & g . 5 = x5 & g . 6 = x6 & g . 7 = x7 & g . 8 = x8 & g . 9 = x9 & g . 10 = x10 & g . 11 = x11 & g . 12 = x12 & g . 13 = x13 & g . 14 = x14 & g . 15 = x15 & g . 16 = x16 & g . 17 = x17 & g . 18 = x18 & g . 19 = x19 & g . 20 = x20 & g . 21 = x21 & g . 22 = x22 & g . 23 = x23 & g . 24 = x24 & g . 25 = x25 & g . 26 = x26 & g . 27 = x27 & g . 28 = x28 & g . 29 = x29 & g . 30 = x30 & g . 31 = x31 & g . 32 = x32 & g . 33 = x33 & g . 34 = x34 & g . 35 = x35 & g . 36 = x36 & g . 37 = x37 & g . 38 = x38 & g . 39 = x39 & g . 40 = x40 & g . 41 = x41 & g . 42 = x42 & g . 43 = x43 & g . 44 = x44 & g . 45 = x45 & g . 46 = x46 & g . 47 = x47 & g . 48 = x48 & g . 49 = x49 & g . 50 = x50 & g . 51 = x51 & g . 52 = x52 & g . 53 = x53 & g . 54 = x54 & g . 55 = x55 & g . 56 = x56 & g . 57 = x57 & g . 58 = x58 & g . 59 = x59 & g . 60 = x60 & g . 61 = x61 & g . 62 = x62 & g . 63 = x63 & g . 0 = x64 holds
f = g

proof end;

definition

func DES-SBOX1 -> Function of 64,16 means :: DESCIP_1:def 6
( it . 0 = 14 & it . 1 = 4 & it . 2 = 13 & it . 3 = 1 & it . 4 = 2 & it . 5 = 15 & it . 6 = 11 & it . 7 = 8 & it . 8 = 3 & it . 9 = 10 & it . 10 = 6 & it . 11 = 12 & it . 12 = 5 & it . 13 = 9 & it . 14 = 0 & it . 15 = 7 & it . 16 = 0 & it . 17 = 15 & it . 18 = 7 & it . 19 = 4 & it . 20 = 14 & it . 21 = 2 & it . 22 = 13 & it . 23 = 1 & it . 24 = 10 & it . 25 = 6 & it . 26 = 12 & it . 27 = 11 & it . 28 = 9 & it . 29 = 5 & it . 30 = 3 & it . 31 = 8 & it . 32 = 4 & it . 33 = 1 & it . 34 = 14 & it . 35 = 8 & it . 36 = 13 & it . 37 = 6 & it . 38 = 2 & it . 39 = 11 & it . 40 = 15 & it . 41 = 12 & it . 42 = 9 & it . 43 = 7 & it . 44 = 3 & it . 45 = 10 & it . 46 = 5 & it . 47 = 0 & it . 48 = 15 & it . 49 = 12 & it . 50 = 8 & it . 51 = 2 & it . 52 = 4 & it . 53 = 9 & it . 54 = 1 & it . 55 = 7 & it . 56 = 5 & it . 57 = 11 & it . 58 = 3 & it . 59 = 14 & it . 60 = 10 & it . 61 = 0 & it . 62 = 6 & it . 63 = 13 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 14 & b₁ . 1 = 4 & b₁ . 2 = 13 & b₁ . 3 = 1 & b₁ . 4 = 2 & b₁ . 5 = 15 & b₁ . 6 = 11 & b₁ . 7 = 8 & b₁ . 8 = 3 & b₁ . 9 = 10 & b₁ . 10 = 6 & b₁ . 11 = 12 & b₁ . 12 = 5 & b₁ . 13 = 9 & b₁ . 14 = 0 & b₁ . 15 = 7 & b₁ . 16 = 0 & b₁ . 17 = 15 & b₁ . 18 = 7 & b₁ . 19 = 4 & b₁ . 20 = 14 & b₁ . 21 = 2 & b₁ . 22 = 13 & b₁ . 23 = 1 & b₁ . 24 = 10 & b₁ . 25 = 6 & b₁ . 26 = 12 & b₁ . 27 = 11 & b₁ . 28 = 9 & b₁ . 29 = 5 & b₁ . 30 = 3 & b₁ . 31 = 8 & b₁ . 32 = 4 & b₁ . 33 = 1 & b₁ . 34 = 14 & b₁ . 35 = 8 & b₁ . 36 = 13 & b₁ . 37 = 6 & b₁ . 38 = 2 & b₁ . 39 = 11 & b₁ . 40 = 15 & b₁ . 41 = 12 & b₁ . 42 = 9 & b₁ . 43 = 7 & b₁ . 44 = 3 & b₁ . 45 = 10 & b₁ . 46 = 5 & b₁ . 47 = 0 & b₁ . 48 = 15 & b₁ . 49 = 12 & b₁ . 50 = 8 & b₁ . 51 = 2 & b₁ . 52 = 4 & b₁ . 53 = 9 & b₁ . 54 = 1 & b₁ . 55 = 7 & b₁ . 56 = 5 & b₁ . 57 = 11 & b₁ . 58 = 3 & b₁ . 59 = 14 & b₁ . 60 = 10 & b₁ . 61 = 0 & b₁ . 62 = 6 & b₁ . 63 = 13 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 14 & b₁ . 1 = 4 & b₁ . 2 = 13 & b₁ . 3 = 1 & b₁ . 4 = 2 & b₁ . 5 = 15 & b₁ . 6 = 11 & b₁ . 7 = 8 & b₁ . 8 = 3 & b₁ . 9 = 10 & b₁ . 10 = 6 & b₁ . 11 = 12 & b₁ . 12 = 5 & b₁ . 13 = 9 & b₁ . 14 = 0 & b₁ . 15 = 7 & b₁ . 16 = 0 & b₁ . 17 = 15 & b₁ . 18 = 7 & b₁ . 19 = 4 & b₁ . 20 = 14 & b₁ . 21 = 2 & b₁ . 22 = 13 & b₁ . 23 = 1 & b₁ . 24 = 10 & b₁ . 25 = 6 & b₁ . 26 = 12 & b₁ . 27 = 11 & b₁ . 28 = 9 & b₁ . 29 = 5 & b₁ . 30 = 3 & b₁ . 31 = 8 & b₁ . 32 = 4 & b₁ . 33 = 1 & b₁ . 34 = 14 & b₁ . 35 = 8 & b₁ . 36 = 13 & b₁ . 37 = 6 & b₁ . 38 = 2 & b₁ . 39 = 11 & b₁ . 40 = 15 & b₁ . 41 = 12 & b₁ . 42 = 9 & b₁ . 43 = 7 & b₁ . 44 = 3 & b₁ . 45 = 10 & b₁ . 46 = 5 & b₁ . 47 = 0 & b₁ . 48 = 15 & b₁ . 49 = 12 & b₁ . 50 = 8 & b₁ . 51 = 2 & b₁ . 52 = 4 & b₁ . 53 = 9 & b₁ . 54 = 1 & b₁ . 55 = 7 & b₁ . 56 = 5 & b₁ . 57 = 11 & b₁ . 58 = 3 & b₁ . 59 = 14 & b₁ . 60 = 10 & b₁ . 61 = 0 & b₁ . 62 = 6 & b₁ . 63 = 13 & b₂ . 0 = 14 & b₂ . 1 = 4 & b₂ . 2 = 13 & b₂ . 3 = 1 & b₂ . 4 = 2 & b₂ . 5 = 15 & b₂ . 6 = 11 & b₂ . 7 = 8 & b₂ . 8 = 3 & b₂ . 9 = 10 & b₂ . 10 = 6 & b₂ . 11 = 12 & b₂ . 12 = 5 & b₂ . 13 = 9 & b₂ . 14 = 0 & b₂ . 15 = 7 & b₂ . 16 = 0 & b₂ . 17 = 15 & b₂ . 18 = 7 & b₂ . 19 = 4 & b₂ . 20 = 14 & b₂ . 21 = 2 & b₂ . 22 = 13 & b₂ . 23 = 1 & b₂ . 24 = 10 & b₂ . 25 = 6 & b₂ . 26 = 12 & b₂ . 27 = 11 & b₂ . 28 = 9 & b₂ . 29 = 5 & b₂ . 30 = 3 & b₂ . 31 = 8 & b₂ . 32 = 4 & b₂ . 33 = 1 & b₂ . 34 = 14 & b₂ . 35 = 8 & b₂ . 36 = 13 & b₂ . 37 = 6 & b₂ . 38 = 2 & b₂ . 39 = 11 & b₂ . 40 = 15 & b₂ . 41 = 12 & b₂ . 42 = 9 & b₂ . 43 = 7 & b₂ . 44 = 3 & b₂ . 45 = 10 & b₂ . 46 = 5 & b₂ . 47 = 0 & b₂ . 48 = 15 & b₂ . 49 = 12 & b₂ . 50 = 8 & b₂ . 51 = 2 & b₂ . 52 = 4 & b₂ . 53 = 9 & b₂ . 54 = 1 & b₂ . 55 = 7 & b₂ . 56 = 5 & b₂ . 57 = 11 & b₂ . 58 = 3 & b₂ . 59 = 14 & b₂ . 60 = 10 & b₂ . 61 = 0 & b₂ . 62 = 6 & b₂ . 63 = 13 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX2 -> Function of 64,16 means :: DESCIP_1:def 7
( it . 0 = 15 & it . 1 = 1 & it . 2 = 8 & it . 3 = 14 & it . 4 = 6 & it . 5 = 11 & it . 6 = 3 & it . 7 = 4 & it . 8 = 9 & it . 9 = 7 & it . 10 = 2 & it . 11 = 13 & it . 12 = 12 & it . 13 = 0 & it . 14 = 5 & it . 15 = 10 & it . 16 = 3 & it . 17 = 13 & it . 18 = 4 & it . 19 = 7 & it . 20 = 15 & it . 21 = 2 & it . 22 = 8 & it . 23 = 14 & it . 24 = 12 & it . 25 = 0 & it . 26 = 1 & it . 27 = 10 & it . 28 = 6 & it . 29 = 9 & it . 30 = 11 & it . 31 = 5 & it . 32 = 0 & it . 33 = 14 & it . 34 = 7 & it . 35 = 11 & it . 36 = 10 & it . 37 = 4 & it . 38 = 13 & it . 39 = 1 & it . 40 = 5 & it . 41 = 8 & it . 42 = 12 & it . 43 = 6 & it . 44 = 9 & it . 45 = 3 & it . 46 = 2 & it . 47 = 15 & it . 48 = 13 & it . 49 = 8 & it . 50 = 10 & it . 51 = 1 & it . 52 = 3 & it . 53 = 15 & it . 54 = 4 & it . 55 = 2 & it . 56 = 11 & it . 57 = 6 & it . 58 = 7 & it . 59 = 12 & it . 60 = 0 & it . 61 = 5 & it . 62 = 14 & it . 63 = 9 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 15 & b₁ . 1 = 1 & b₁ . 2 = 8 & b₁ . 3 = 14 & b₁ . 4 = 6 & b₁ . 5 = 11 & b₁ . 6 = 3 & b₁ . 7 = 4 & b₁ . 8 = 9 & b₁ . 9 = 7 & b₁ . 10 = 2 & b₁ . 11 = 13 & b₁ . 12 = 12 & b₁ . 13 = 0 & b₁ . 14 = 5 & b₁ . 15 = 10 & b₁ . 16 = 3 & b₁ . 17 = 13 & b₁ . 18 = 4 & b₁ . 19 = 7 & b₁ . 20 = 15 & b₁ . 21 = 2 & b₁ . 22 = 8 & b₁ . 23 = 14 & b₁ . 24 = 12 & b₁ . 25 = 0 & b₁ . 26 = 1 & b₁ . 27 = 10 & b₁ . 28 = 6 & b₁ . 29 = 9 & b₁ . 30 = 11 & b₁ . 31 = 5 & b₁ . 32 = 0 & b₁ . 33 = 14 & b₁ . 34 = 7 & b₁ . 35 = 11 & b₁ . 36 = 10 & b₁ . 37 = 4 & b₁ . 38 = 13 & b₁ . 39 = 1 & b₁ . 40 = 5 & b₁ . 41 = 8 & b₁ . 42 = 12 & b₁ . 43 = 6 & b₁ . 44 = 9 & b₁ . 45 = 3 & b₁ . 46 = 2 & b₁ . 47 = 15 & b₁ . 48 = 13 & b₁ . 49 = 8 & b₁ . 50 = 10 & b₁ . 51 = 1 & b₁ . 52 = 3 & b₁ . 53 = 15 & b₁ . 54 = 4 & b₁ . 55 = 2 & b₁ . 56 = 11 & b₁ . 57 = 6 & b₁ . 58 = 7 & b₁ . 59 = 12 & b₁ . 60 = 0 & b₁ . 61 = 5 & b₁ . 62 = 14 & b₁ . 63 = 9 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 15 & b₁ . 1 = 1 & b₁ . 2 = 8 & b₁ . 3 = 14 & b₁ . 4 = 6 & b₁ . 5 = 11 & b₁ . 6 = 3 & b₁ . 7 = 4 & b₁ . 8 = 9 & b₁ . 9 = 7 & b₁ . 10 = 2 & b₁ . 11 = 13 & b₁ . 12 = 12 & b₁ . 13 = 0 & b₁ . 14 = 5 & b₁ . 15 = 10 & b₁ . 16 = 3 & b₁ . 17 = 13 & b₁ . 18 = 4 & b₁ . 19 = 7 & b₁ . 20 = 15 & b₁ . 21 = 2 & b₁ . 22 = 8 & b₁ . 23 = 14 & b₁ . 24 = 12 & b₁ . 25 = 0 & b₁ . 26 = 1 & b₁ . 27 = 10 & b₁ . 28 = 6 & b₁ . 29 = 9 & b₁ . 30 = 11 & b₁ . 31 = 5 & b₁ . 32 = 0 & b₁ . 33 = 14 & b₁ . 34 = 7 & b₁ . 35 = 11 & b₁ . 36 = 10 & b₁ . 37 = 4 & b₁ . 38 = 13 & b₁ . 39 = 1 & b₁ . 40 = 5 & b₁ . 41 = 8 & b₁ . 42 = 12 & b₁ . 43 = 6 & b₁ . 44 = 9 & b₁ . 45 = 3 & b₁ . 46 = 2 & b₁ . 47 = 15 & b₁ . 48 = 13 & b₁ . 49 = 8 & b₁ . 50 = 10 & b₁ . 51 = 1 & b₁ . 52 = 3 & b₁ . 53 = 15 & b₁ . 54 = 4 & b₁ . 55 = 2 & b₁ . 56 = 11 & b₁ . 57 = 6 & b₁ . 58 = 7 & b₁ . 59 = 12 & b₁ . 60 = 0 & b₁ . 61 = 5 & b₁ . 62 = 14 & b₁ . 63 = 9 & b₂ . 0 = 15 & b₂ . 1 = 1 & b₂ . 2 = 8 & b₂ . 3 = 14 & b₂ . 4 = 6 & b₂ . 5 = 11 & b₂ . 6 = 3 & b₂ . 7 = 4 & b₂ . 8 = 9 & b₂ . 9 = 7 & b₂ . 10 = 2 & b₂ . 11 = 13 & b₂ . 12 = 12 & b₂ . 13 = 0 & b₂ . 14 = 5 & b₂ . 15 = 10 & b₂ . 16 = 3 & b₂ . 17 = 13 & b₂ . 18 = 4 & b₂ . 19 = 7 & b₂ . 20 = 15 & b₂ . 21 = 2 & b₂ . 22 = 8 & b₂ . 23 = 14 & b₂ . 24 = 12 & b₂ . 25 = 0 & b₂ . 26 = 1 & b₂ . 27 = 10 & b₂ . 28 = 6 & b₂ . 29 = 9 & b₂ . 30 = 11 & b₂ . 31 = 5 & b₂ . 32 = 0 & b₂ . 33 = 14 & b₂ . 34 = 7 & b₂ . 35 = 11 & b₂ . 36 = 10 & b₂ . 37 = 4 & b₂ . 38 = 13 & b₂ . 39 = 1 & b₂ . 40 = 5 & b₂ . 41 = 8 & b₂ . 42 = 12 & b₂ . 43 = 6 & b₂ . 44 = 9 & b₂ . 45 = 3 & b₂ . 46 = 2 & b₂ . 47 = 15 & b₂ . 48 = 13 & b₂ . 49 = 8 & b₂ . 50 = 10 & b₂ . 51 = 1 & b₂ . 52 = 3 & b₂ . 53 = 15 & b₂ . 54 = 4 & b₂ . 55 = 2 & b₂ . 56 = 11 & b₂ . 57 = 6 & b₂ . 58 = 7 & b₂ . 59 = 12 & b₂ . 60 = 0 & b₂ . 61 = 5 & b₂ . 62 = 14 & b₂ . 63 = 9 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX3 -> Function of 64,16 means :: DESCIP_1:def 8
( it . 0 = 10 & it . 1 = 0 & it . 2 = 9 & it . 3 = 14 & it . 4 = 6 & it . 5 = 3 & it . 6 = 15 & it . 7 = 5 & it . 8 = 1 & it . 9 = 13 & it . 10 = 12 & it . 11 = 7 & it . 12 = 11 & it . 13 = 4 & it . 14 = 2 & it . 15 = 8 & it . 16 = 13 & it . 17 = 7 & it . 18 = 0 & it . 19 = 9 & it . 20 = 3 & it . 21 = 4 & it . 22 = 6 & it . 23 = 10 & it . 24 = 2 & it . 25 = 8 & it . 26 = 5 & it . 27 = 14 & it . 28 = 12 & it . 29 = 11 & it . 30 = 15 & it . 31 = 1 & it . 32 = 13 & it . 33 = 6 & it . 34 = 4 & it . 35 = 9 & it . 36 = 8 & it . 37 = 15 & it . 38 = 3 & it . 39 = 0 & it . 40 = 11 & it . 41 = 1 & it . 42 = 2 & it . 43 = 12 & it . 44 = 5 & it . 45 = 10 & it . 46 = 14 & it . 47 = 7 & it . 48 = 1 & it . 49 = 10 & it . 50 = 13 & it . 51 = 0 & it . 52 = 6 & it . 53 = 9 & it . 54 = 8 & it . 55 = 7 & it . 56 = 4 & it . 57 = 15 & it . 58 = 14 & it . 59 = 3 & it . 60 = 11 & it . 61 = 5 & it . 62 = 2 & it . 63 = 12 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 10 & b₁ . 1 = 0 & b₁ . 2 = 9 & b₁ . 3 = 14 & b₁ . 4 = 6 & b₁ . 5 = 3 & b₁ . 6 = 15 & b₁ . 7 = 5 & b₁ . 8 = 1 & b₁ . 9 = 13 & b₁ . 10 = 12 & b₁ . 11 = 7 & b₁ . 12 = 11 & b₁ . 13 = 4 & b₁ . 14 = 2 & b₁ . 15 = 8 & b₁ . 16 = 13 & b₁ . 17 = 7 & b₁ . 18 = 0 & b₁ . 19 = 9 & b₁ . 20 = 3 & b₁ . 21 = 4 & b₁ . 22 = 6 & b₁ . 23 = 10 & b₁ . 24 = 2 & b₁ . 25 = 8 & b₁ . 26 = 5 & b₁ . 27 = 14 & b₁ . 28 = 12 & b₁ . 29 = 11 & b₁ . 30 = 15 & b₁ . 31 = 1 & b₁ . 32 = 13 & b₁ . 33 = 6 & b₁ . 34 = 4 & b₁ . 35 = 9 & b₁ . 36 = 8 & b₁ . 37 = 15 & b₁ . 38 = 3 & b₁ . 39 = 0 & b₁ . 40 = 11 & b₁ . 41 = 1 & b₁ . 42 = 2 & b₁ . 43 = 12 & b₁ . 44 = 5 & b₁ . 45 = 10 & b₁ . 46 = 14 & b₁ . 47 = 7 & b₁ . 48 = 1 & b₁ . 49 = 10 & b₁ . 50 = 13 & b₁ . 51 = 0 & b₁ . 52 = 6 & b₁ . 53 = 9 & b₁ . 54 = 8 & b₁ . 55 = 7 & b₁ . 56 = 4 & b₁ . 57 = 15 & b₁ . 58 = 14 & b₁ . 59 = 3 & b₁ . 60 = 11 & b₁ . 61 = 5 & b₁ . 62 = 2 & b₁ . 63 = 12 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 10 & b₁ . 1 = 0 & b₁ . 2 = 9 & b₁ . 3 = 14 & b₁ . 4 = 6 & b₁ . 5 = 3 & b₁ . 6 = 15 & b₁ . 7 = 5 & b₁ . 8 = 1 & b₁ . 9 = 13 & b₁ . 10 = 12 & b₁ . 11 = 7 & b₁ . 12 = 11 & b₁ . 13 = 4 & b₁ . 14 = 2 & b₁ . 15 = 8 & b₁ . 16 = 13 & b₁ . 17 = 7 & b₁ . 18 = 0 & b₁ . 19 = 9 & b₁ . 20 = 3 & b₁ . 21 = 4 & b₁ . 22 = 6 & b₁ . 23 = 10 & b₁ . 24 = 2 & b₁ . 25 = 8 & b₁ . 26 = 5 & b₁ . 27 = 14 & b₁ . 28 = 12 & b₁ . 29 = 11 & b₁ . 30 = 15 & b₁ . 31 = 1 & b₁ . 32 = 13 & b₁ . 33 = 6 & b₁ . 34 = 4 & b₁ . 35 = 9 & b₁ . 36 = 8 & b₁ . 37 = 15 & b₁ . 38 = 3 & b₁ . 39 = 0 & b₁ . 40 = 11 & b₁ . 41 = 1 & b₁ . 42 = 2 & b₁ . 43 = 12 & b₁ . 44 = 5 & b₁ . 45 = 10 & b₁ . 46 = 14 & b₁ . 47 = 7 & b₁ . 48 = 1 & b₁ . 49 = 10 & b₁ . 50 = 13 & b₁ . 51 = 0 & b₁ . 52 = 6 & b₁ . 53 = 9 & b₁ . 54 = 8 & b₁ . 55 = 7 & b₁ . 56 = 4 & b₁ . 57 = 15 & b₁ . 58 = 14 & b₁ . 59 = 3 & b₁ . 60 = 11 & b₁ . 61 = 5 & b₁ . 62 = 2 & b₁ . 63 = 12 & b₂ . 0 = 10 & b₂ . 1 = 0 & b₂ . 2 = 9 & b₂ . 3 = 14 & b₂ . 4 = 6 & b₂ . 5 = 3 & b₂ . 6 = 15 & b₂ . 7 = 5 & b₂ . 8 = 1 & b₂ . 9 = 13 & b₂ . 10 = 12 & b₂ . 11 = 7 & b₂ . 12 = 11 & b₂ . 13 = 4 & b₂ . 14 = 2 & b₂ . 15 = 8 & b₂ . 16 = 13 & b₂ . 17 = 7 & b₂ . 18 = 0 & b₂ . 19 = 9 & b₂ . 20 = 3 & b₂ . 21 = 4 & b₂ . 22 = 6 & b₂ . 23 = 10 & b₂ . 24 = 2 & b₂ . 25 = 8 & b₂ . 26 = 5 & b₂ . 27 = 14 & b₂ . 28 = 12 & b₂ . 29 = 11 & b₂ . 30 = 15 & b₂ . 31 = 1 & b₂ . 32 = 13 & b₂ . 33 = 6 & b₂ . 34 = 4 & b₂ . 35 = 9 & b₂ . 36 = 8 & b₂ . 37 = 15 & b₂ . 38 = 3 & b₂ . 39 = 0 & b₂ . 40 = 11 & b₂ . 41 = 1 & b₂ . 42 = 2 & b₂ . 43 = 12 & b₂ . 44 = 5 & b₂ . 45 = 10 & b₂ . 46 = 14 & b₂ . 47 = 7 & b₂ . 48 = 1 & b₂ . 49 = 10 & b₂ . 50 = 13 & b₂ . 51 = 0 & b₂ . 52 = 6 & b₂ . 53 = 9 & b₂ . 54 = 8 & b₂ . 55 = 7 & b₂ . 56 = 4 & b₂ . 57 = 15 & b₂ . 58 = 14 & b₂ . 59 = 3 & b₂ . 60 = 11 & b₂ . 61 = 5 & b₂ . 62 = 2 & b₂ . 63 = 12 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX4 -> Function of 64,16 means :: DESCIP_1:def 9
( it . 0 = 7 & it . 1 = 13 & it . 2 = 14 & it . 3 = 3 & it . 4 = 0 & it . 5 = 6 & it . 6 = 9 & it . 7 = 10 & it . 8 = 1 & it . 9 = 2 & it . 10 = 8 & it . 11 = 5 & it . 12 = 11 & it . 13 = 12 & it . 14 = 4 & it . 15 = 15 & it . 16 = 13 & it . 17 = 8 & it . 18 = 11 & it . 19 = 5 & it . 20 = 6 & it . 21 = 15 & it . 22 = 0 & it . 23 = 3 & it . 24 = 4 & it . 25 = 7 & it . 26 = 2 & it . 27 = 12 & it . 28 = 1 & it . 29 = 10 & it . 30 = 14 & it . 31 = 9 & it . 32 = 10 & it . 33 = 6 & it . 34 = 9 & it . 35 = 0 & it . 36 = 12 & it . 37 = 11 & it . 38 = 7 & it . 39 = 13 & it . 40 = 15 & it . 41 = 1 & it . 42 = 3 & it . 43 = 14 & it . 44 = 5 & it . 45 = 2 & it . 46 = 8 & it . 47 = 4 & it . 48 = 3 & it . 49 = 15 & it . 50 = 0 & it . 51 = 6 & it . 52 = 10 & it . 53 = 1 & it . 54 = 13 & it . 55 = 8 & it . 56 = 9 & it . 57 = 4 & it . 58 = 5 & it . 59 = 11 & it . 60 = 12 & it . 61 = 7 & it . 62 = 2 & it . 63 = 14 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 7 & b₁ . 1 = 13 & b₁ . 2 = 14 & b₁ . 3 = 3 & b₁ . 4 = 0 & b₁ . 5 = 6 & b₁ . 6 = 9 & b₁ . 7 = 10 & b₁ . 8 = 1 & b₁ . 9 = 2 & b₁ . 10 = 8 & b₁ . 11 = 5 & b₁ . 12 = 11 & b₁ . 13 = 12 & b₁ . 14 = 4 & b₁ . 15 = 15 & b₁ . 16 = 13 & b₁ . 17 = 8 & b₁ . 18 = 11 & b₁ . 19 = 5 & b₁ . 20 = 6 & b₁ . 21 = 15 & b₁ . 22 = 0 & b₁ . 23 = 3 & b₁ . 24 = 4 & b₁ . 25 = 7 & b₁ . 26 = 2 & b₁ . 27 = 12 & b₁ . 28 = 1 & b₁ . 29 = 10 & b₁ . 30 = 14 & b₁ . 31 = 9 & b₁ . 32 = 10 & b₁ . 33 = 6 & b₁ . 34 = 9 & b₁ . 35 = 0 & b₁ . 36 = 12 & b₁ . 37 = 11 & b₁ . 38 = 7 & b₁ . 39 = 13 & b₁ . 40 = 15 & b₁ . 41 = 1 & b₁ . 42 = 3 & b₁ . 43 = 14 & b₁ . 44 = 5 & b₁ . 45 = 2 & b₁ . 46 = 8 & b₁ . 47 = 4 & b₁ . 48 = 3 & b₁ . 49 = 15 & b₁ . 50 = 0 & b₁ . 51 = 6 & b₁ . 52 = 10 & b₁ . 53 = 1 & b₁ . 54 = 13 & b₁ . 55 = 8 & b₁ . 56 = 9 & b₁ . 57 = 4 & b₁ . 58 = 5 & b₁ . 59 = 11 & b₁ . 60 = 12 & b₁ . 61 = 7 & b₁ . 62 = 2 & b₁ . 63 = 14 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 7 & b₁ . 1 = 13 & b₁ . 2 = 14 & b₁ . 3 = 3 & b₁ . 4 = 0 & b₁ . 5 = 6 & b₁ . 6 = 9 & b₁ . 7 = 10 & b₁ . 8 = 1 & b₁ . 9 = 2 & b₁ . 10 = 8 & b₁ . 11 = 5 & b₁ . 12 = 11 & b₁ . 13 = 12 & b₁ . 14 = 4 & b₁ . 15 = 15 & b₁ . 16 = 13 & b₁ . 17 = 8 & b₁ . 18 = 11 & b₁ . 19 = 5 & b₁ . 20 = 6 & b₁ . 21 = 15 & b₁ . 22 = 0 & b₁ . 23 = 3 & b₁ . 24 = 4 & b₁ . 25 = 7 & b₁ . 26 = 2 & b₁ . 27 = 12 & b₁ . 28 = 1 & b₁ . 29 = 10 & b₁ . 30 = 14 & b₁ . 31 = 9 & b₁ . 32 = 10 & b₁ . 33 = 6 & b₁ . 34 = 9 & b₁ . 35 = 0 & b₁ . 36 = 12 & b₁ . 37 = 11 & b₁ . 38 = 7 & b₁ . 39 = 13 & b₁ . 40 = 15 & b₁ . 41 = 1 & b₁ . 42 = 3 & b₁ . 43 = 14 & b₁ . 44 = 5 & b₁ . 45 = 2 & b₁ . 46 = 8 & b₁ . 47 = 4 & b₁ . 48 = 3 & b₁ . 49 = 15 & b₁ . 50 = 0 & b₁ . 51 = 6 & b₁ . 52 = 10 & b₁ . 53 = 1 & b₁ . 54 = 13 & b₁ . 55 = 8 & b₁ . 56 = 9 & b₁ . 57 = 4 & b₁ . 58 = 5 & b₁ . 59 = 11 & b₁ . 60 = 12 & b₁ . 61 = 7 & b₁ . 62 = 2 & b₁ . 63 = 14 & b₂ . 0 = 7 & b₂ . 1 = 13 & b₂ . 2 = 14 & b₂ . 3 = 3 & b₂ . 4 = 0 & b₂ . 5 = 6 & b₂ . 6 = 9 & b₂ . 7 = 10 & b₂ . 8 = 1 & b₂ . 9 = 2 & b₂ . 10 = 8 & b₂ . 11 = 5 & b₂ . 12 = 11 & b₂ . 13 = 12 & b₂ . 14 = 4 & b₂ . 15 = 15 & b₂ . 16 = 13 & b₂ . 17 = 8 & b₂ . 18 = 11 & b₂ . 19 = 5 & b₂ . 20 = 6 & b₂ . 21 = 15 & b₂ . 22 = 0 & b₂ . 23 = 3 & b₂ . 24 = 4 & b₂ . 25 = 7 & b₂ . 26 = 2 & b₂ . 27 = 12 & b₂ . 28 = 1 & b₂ . 29 = 10 & b₂ . 30 = 14 & b₂ . 31 = 9 & b₂ . 32 = 10 & b₂ . 33 = 6 & b₂ . 34 = 9 & b₂ . 35 = 0 & b₂ . 36 = 12 & b₂ . 37 = 11 & b₂ . 38 = 7 & b₂ . 39 = 13 & b₂ . 40 = 15 & b₂ . 41 = 1 & b₂ . 42 = 3 & b₂ . 43 = 14 & b₂ . 44 = 5 & b₂ . 45 = 2 & b₂ . 46 = 8 & b₂ . 47 = 4 & b₂ . 48 = 3 & b₂ . 49 = 15 & b₂ . 50 = 0 & b₂ . 51 = 6 & b₂ . 52 = 10 & b₂ . 53 = 1 & b₂ . 54 = 13 & b₂ . 55 = 8 & b₂ . 56 = 9 & b₂ . 57 = 4 & b₂ . 58 = 5 & b₂ . 59 = 11 & b₂ . 60 = 12 & b₂ . 61 = 7 & b₂ . 62 = 2 & b₂ . 63 = 14 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX5 -> Function of 64,16 means :: DESCIP_1:def 10
( it . 0 = 2 & it . 1 = 12 & it . 2 = 4 & it . 3 = 1 & it . 4 = 7 & it . 5 = 10 & it . 6 = 11 & it . 7 = 6 & it . 8 = 8 & it . 9 = 5 & it . 10 = 3 & it . 11 = 15 & it . 12 = 13 & it . 13 = 0 & it . 14 = 14 & it . 15 = 9 & it . 16 = 14 & it . 17 = 11 & it . 18 = 2 & it . 19 = 12 & it . 20 = 4 & it . 21 = 7 & it . 22 = 13 & it . 23 = 1 & it . 24 = 5 & it . 25 = 0 & it . 26 = 15 & it . 27 = 10 & it . 28 = 3 & it . 29 = 9 & it . 30 = 8 & it . 31 = 6 & it . 32 = 4 & it . 33 = 2 & it . 34 = 1 & it . 35 = 11 & it . 36 = 10 & it . 37 = 13 & it . 38 = 7 & it . 39 = 8 & it . 40 = 15 & it . 41 = 9 & it . 42 = 12 & it . 43 = 5 & it . 44 = 6 & it . 45 = 3 & it . 46 = 0 & it . 47 = 14 & it . 48 = 11 & it . 49 = 8 & it . 50 = 12 & it . 51 = 7 & it . 52 = 1 & it . 53 = 14 & it . 54 = 2 & it . 55 = 13 & it . 56 = 6 & it . 57 = 15 & it . 58 = 0 & it . 59 = 9 & it . 60 = 10 & it . 61 = 4 & it . 62 = 5 & it . 63 = 3 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 2 & b₁ . 1 = 12 & b₁ . 2 = 4 & b₁ . 3 = 1 & b₁ . 4 = 7 & b₁ . 5 = 10 & b₁ . 6 = 11 & b₁ . 7 = 6 & b₁ . 8 = 8 & b₁ . 9 = 5 & b₁ . 10 = 3 & b₁ . 11 = 15 & b₁ . 12 = 13 & b₁ . 13 = 0 & b₁ . 14 = 14 & b₁ . 15 = 9 & b₁ . 16 = 14 & b₁ . 17 = 11 & b₁ . 18 = 2 & b₁ . 19 = 12 & b₁ . 20 = 4 & b₁ . 21 = 7 & b₁ . 22 = 13 & b₁ . 23 = 1 & b₁ . 24 = 5 & b₁ . 25 = 0 & b₁ . 26 = 15 & b₁ . 27 = 10 & b₁ . 28 = 3 & b₁ . 29 = 9 & b₁ . 30 = 8 & b₁ . 31 = 6 & b₁ . 32 = 4 & b₁ . 33 = 2 & b₁ . 34 = 1 & b₁ . 35 = 11 & b₁ . 36 = 10 & b₁ . 37 = 13 & b₁ . 38 = 7 & b₁ . 39 = 8 & b₁ . 40 = 15 & b₁ . 41 = 9 & b₁ . 42 = 12 & b₁ . 43 = 5 & b₁ . 44 = 6 & b₁ . 45 = 3 & b₁ . 46 = 0 & b₁ . 47 = 14 & b₁ . 48 = 11 & b₁ . 49 = 8 & b₁ . 50 = 12 & b₁ . 51 = 7 & b₁ . 52 = 1 & b₁ . 53 = 14 & b₁ . 54 = 2 & b₁ . 55 = 13 & b₁ . 56 = 6 & b₁ . 57 = 15 & b₁ . 58 = 0 & b₁ . 59 = 9 & b₁ . 60 = 10 & b₁ . 61 = 4 & b₁ . 62 = 5 & b₁ . 63 = 3 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 2 & b₁ . 1 = 12 & b₁ . 2 = 4 & b₁ . 3 = 1 & b₁ . 4 = 7 & b₁ . 5 = 10 & b₁ . 6 = 11 & b₁ . 7 = 6 & b₁ . 8 = 8 & b₁ . 9 = 5 & b₁ . 10 = 3 & b₁ . 11 = 15 & b₁ . 12 = 13 & b₁ . 13 = 0 & b₁ . 14 = 14 & b₁ . 15 = 9 & b₁ . 16 = 14 & b₁ . 17 = 11 & b₁ . 18 = 2 & b₁ . 19 = 12 & b₁ . 20 = 4 & b₁ . 21 = 7 & b₁ . 22 = 13 & b₁ . 23 = 1 & b₁ . 24 = 5 & b₁ . 25 = 0 & b₁ . 26 = 15 & b₁ . 27 = 10 & b₁ . 28 = 3 & b₁ . 29 = 9 & b₁ . 30 = 8 & b₁ . 31 = 6 & b₁ . 32 = 4 & b₁ . 33 = 2 & b₁ . 34 = 1 & b₁ . 35 = 11 & b₁ . 36 = 10 & b₁ . 37 = 13 & b₁ . 38 = 7 & b₁ . 39 = 8 & b₁ . 40 = 15 & b₁ . 41 = 9 & b₁ . 42 = 12 & b₁ . 43 = 5 & b₁ . 44 = 6 & b₁ . 45 = 3 & b₁ . 46 = 0 & b₁ . 47 = 14 & b₁ . 48 = 11 & b₁ . 49 = 8 & b₁ . 50 = 12 & b₁ . 51 = 7 & b₁ . 52 = 1 & b₁ . 53 = 14 & b₁ . 54 = 2 & b₁ . 55 = 13 & b₁ . 56 = 6 & b₁ . 57 = 15 & b₁ . 58 = 0 & b₁ . 59 = 9 & b₁ . 60 = 10 & b₁ . 61 = 4 & b₁ . 62 = 5 & b₁ . 63 = 3 & b₂ . 0 = 2 & b₂ . 1 = 12 & b₂ . 2 = 4 & b₂ . 3 = 1 & b₂ . 4 = 7 & b₂ . 5 = 10 & b₂ . 6 = 11 & b₂ . 7 = 6 & b₂ . 8 = 8 & b₂ . 9 = 5 & b₂ . 10 = 3 & b₂ . 11 = 15 & b₂ . 12 = 13 & b₂ . 13 = 0 & b₂ . 14 = 14 & b₂ . 15 = 9 & b₂ . 16 = 14 & b₂ . 17 = 11 & b₂ . 18 = 2 & b₂ . 19 = 12 & b₂ . 20 = 4 & b₂ . 21 = 7 & b₂ . 22 = 13 & b₂ . 23 = 1 & b₂ . 24 = 5 & b₂ . 25 = 0 & b₂ . 26 = 15 & b₂ . 27 = 10 & b₂ . 28 = 3 & b₂ . 29 = 9 & b₂ . 30 = 8 & b₂ . 31 = 6 & b₂ . 32 = 4 & b₂ . 33 = 2 & b₂ . 34 = 1 & b₂ . 35 = 11 & b₂ . 36 = 10 & b₂ . 37 = 13 & b₂ . 38 = 7 & b₂ . 39 = 8 & b₂ . 40 = 15 & b₂ . 41 = 9 & b₂ . 42 = 12 & b₂ . 43 = 5 & b₂ . 44 = 6 & b₂ . 45 = 3 & b₂ . 46 = 0 & b₂ . 47 = 14 & b₂ . 48 = 11 & b₂ . 49 = 8 & b₂ . 50 = 12 & b₂ . 51 = 7 & b₂ . 52 = 1 & b₂ . 53 = 14 & b₂ . 54 = 2 & b₂ . 55 = 13 & b₂ . 56 = 6 & b₂ . 57 = 15 & b₂ . 58 = 0 & b₂ . 59 = 9 & b₂ . 60 = 10 & b₂ . 61 = 4 & b₂ . 62 = 5 & b₂ . 63 = 3 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX6 -> Function of 64,16 means :: DESCIP_1:def 11
( it . 0 = 12 & it . 1 = 1 & it . 2 = 10 & it . 3 = 15 & it . 4 = 9 & it . 5 = 2 & it . 6 = 6 & it . 7 = 8 & it . 8 = 0 & it . 9 = 13 & it . 10 = 3 & it . 11 = 4 & it . 12 = 14 & it . 13 = 7 & it . 14 = 5 & it . 15 = 11 & it . 16 = 10 & it . 17 = 15 & it . 18 = 4 & it . 19 = 2 & it . 20 = 7 & it . 21 = 12 & it . 22 = 9 & it . 23 = 5 & it . 24 = 6 & it . 25 = 1 & it . 26 = 13 & it . 27 = 14 & it . 28 = 0 & it . 29 = 11 & it . 30 = 3 & it . 31 = 8 & it . 32 = 9 & it . 33 = 14 & it . 34 = 15 & it . 35 = 5 & it . 36 = 2 & it . 37 = 8 & it . 38 = 12 & it . 39 = 3 & it . 40 = 7 & it . 41 = 0 & it . 42 = 4 & it . 43 = 10 & it . 44 = 1 & it . 45 = 13 & it . 46 = 11 & it . 47 = 6 & it . 48 = 4 & it . 49 = 3 & it . 50 = 2 & it . 51 = 12 & it . 52 = 9 & it . 53 = 5 & it . 54 = 15 & it . 55 = 10 & it . 56 = 11 & it . 57 = 14 & it . 58 = 1 & it . 59 = 7 & it . 60 = 6 & it . 61 = 0 & it . 62 = 8 & it . 63 = 13 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 12 & b₁ . 1 = 1 & b₁ . 2 = 10 & b₁ . 3 = 15 & b₁ . 4 = 9 & b₁ . 5 = 2 & b₁ . 6 = 6 & b₁ . 7 = 8 & b₁ . 8 = 0 & b₁ . 9 = 13 & b₁ . 10 = 3 & b₁ . 11 = 4 & b₁ . 12 = 14 & b₁ . 13 = 7 & b₁ . 14 = 5 & b₁ . 15 = 11 & b₁ . 16 = 10 & b₁ . 17 = 15 & b₁ . 18 = 4 & b₁ . 19 = 2 & b₁ . 20 = 7 & b₁ . 21 = 12 & b₁ . 22 = 9 & b₁ . 23 = 5 & b₁ . 24 = 6 & b₁ . 25 = 1 & b₁ . 26 = 13 & b₁ . 27 = 14 & b₁ . 28 = 0 & b₁ . 29 = 11 & b₁ . 30 = 3 & b₁ . 31 = 8 & b₁ . 32 = 9 & b₁ . 33 = 14 & b₁ . 34 = 15 & b₁ . 35 = 5 & b₁ . 36 = 2 & b₁ . 37 = 8 & b₁ . 38 = 12 & b₁ . 39 = 3 & b₁ . 40 = 7 & b₁ . 41 = 0 & b₁ . 42 = 4 & b₁ . 43 = 10 & b₁ . 44 = 1 & b₁ . 45 = 13 & b₁ . 46 = 11 & b₁ . 47 = 6 & b₁ . 48 = 4 & b₁ . 49 = 3 & b₁ . 50 = 2 & b₁ . 51 = 12 & b₁ . 52 = 9 & b₁ . 53 = 5 & b₁ . 54 = 15 & b₁ . 55 = 10 & b₁ . 56 = 11 & b₁ . 57 = 14 & b₁ . 58 = 1 & b₁ . 59 = 7 & b₁ . 60 = 6 & b₁ . 61 = 0 & b₁ . 62 = 8 & b₁ . 63 = 13 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 12 & b₁ . 1 = 1 & b₁ . 2 = 10 & b₁ . 3 = 15 & b₁ . 4 = 9 & b₁ . 5 = 2 & b₁ . 6 = 6 & b₁ . 7 = 8 & b₁ . 8 = 0 & b₁ . 9 = 13 & b₁ . 10 = 3 & b₁ . 11 = 4 & b₁ . 12 = 14 & b₁ . 13 = 7 & b₁ . 14 = 5 & b₁ . 15 = 11 & b₁ . 16 = 10 & b₁ . 17 = 15 & b₁ . 18 = 4 & b₁ . 19 = 2 & b₁ . 20 = 7 & b₁ . 21 = 12 & b₁ . 22 = 9 & b₁ . 23 = 5 & b₁ . 24 = 6 & b₁ . 25 = 1 & b₁ . 26 = 13 & b₁ . 27 = 14 & b₁ . 28 = 0 & b₁ . 29 = 11 & b₁ . 30 = 3 & b₁ . 31 = 8 & b₁ . 32 = 9 & b₁ . 33 = 14 & b₁ . 34 = 15 & b₁ . 35 = 5 & b₁ . 36 = 2 & b₁ . 37 = 8 & b₁ . 38 = 12 & b₁ . 39 = 3 & b₁ . 40 = 7 & b₁ . 41 = 0 & b₁ . 42 = 4 & b₁ . 43 = 10 & b₁ . 44 = 1 & b₁ . 45 = 13 & b₁ . 46 = 11 & b₁ . 47 = 6 & b₁ . 48 = 4 & b₁ . 49 = 3 & b₁ . 50 = 2 & b₁ . 51 = 12 & b₁ . 52 = 9 & b₁ . 53 = 5 & b₁ . 54 = 15 & b₁ . 55 = 10 & b₁ . 56 = 11 & b₁ . 57 = 14 & b₁ . 58 = 1 & b₁ . 59 = 7 & b₁ . 60 = 6 & b₁ . 61 = 0 & b₁ . 62 = 8 & b₁ . 63 = 13 & b₂ . 0 = 12 & b₂ . 1 = 1 & b₂ . 2 = 10 & b₂ . 3 = 15 & b₂ . 4 = 9 & b₂ . 5 = 2 & b₂ . 6 = 6 & b₂ . 7 = 8 & b₂ . 8 = 0 & b₂ . 9 = 13 & b₂ . 10 = 3 & b₂ . 11 = 4 & b₂ . 12 = 14 & b₂ . 13 = 7 & b₂ . 14 = 5 & b₂ . 15 = 11 & b₂ . 16 = 10 & b₂ . 17 = 15 & b₂ . 18 = 4 & b₂ . 19 = 2 & b₂ . 20 = 7 & b₂ . 21 = 12 & b₂ . 22 = 9 & b₂ . 23 = 5 & b₂ . 24 = 6 & b₂ . 25 = 1 & b₂ . 26 = 13 & b₂ . 27 = 14 & b₂ . 28 = 0 & b₂ . 29 = 11 & b₂ . 30 = 3 & b₂ . 31 = 8 & b₂ . 32 = 9 & b₂ . 33 = 14 & b₂ . 34 = 15 & b₂ . 35 = 5 & b₂ . 36 = 2 & b₂ . 37 = 8 & b₂ . 38 = 12 & b₂ . 39 = 3 & b₂ . 40 = 7 & b₂ . 41 = 0 & b₂ . 42 = 4 & b₂ . 43 = 10 & b₂ . 44 = 1 & b₂ . 45 = 13 & b₂ . 46 = 11 & b₂ . 47 = 6 & b₂ . 48 = 4 & b₂ . 49 = 3 & b₂ . 50 = 2 & b₂ . 51 = 12 & b₂ . 52 = 9 & b₂ . 53 = 5 & b₂ . 54 = 15 & b₂ . 55 = 10 & b₂ . 56 = 11 & b₂ . 57 = 14 & b₂ . 58 = 1 & b₂ . 59 = 7 & b₂ . 60 = 6 & b₂ . 61 = 0 & b₂ . 62 = 8 & b₂ . 63 = 13 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX7 -> Function of 64,16 means :: DESCIP_1:def 12
( it . 0 = 4 & it . 1 = 11 & it . 2 = 2 & it . 3 = 14 & it . 4 = 15 & it . 5 = 0 & it . 6 = 8 & it . 7 = 13 & it . 8 = 3 & it . 9 = 12 & it . 10 = 9 & it . 11 = 7 & it . 12 = 5 & it . 13 = 10 & it . 14 = 6 & it . 15 = 1 & it . 16 = 13 & it . 17 = 0 & it . 18 = 11 & it . 19 = 7 & it . 20 = 4 & it . 21 = 9 & it . 22 = 1 & it . 23 = 10 & it . 24 = 14 & it . 25 = 3 & it . 26 = 5 & it . 27 = 12 & it . 28 = 2 & it . 29 = 15 & it . 30 = 8 & it . 31 = 6 & it . 32 = 1 & it . 33 = 4 & it . 34 = 11 & it . 35 = 13 & it . 36 = 12 & it . 37 = 3 & it . 38 = 7 & it . 39 = 14 & it . 40 = 10 & it . 41 = 15 & it . 42 = 6 & it . 43 = 8 & it . 44 = 0 & it . 45 = 5 & it . 46 = 9 & it . 47 = 2 & it . 48 = 6 & it . 49 = 11 & it . 50 = 13 & it . 51 = 8 & it . 52 = 1 & it . 53 = 4 & it . 54 = 10 & it . 55 = 7 & it . 56 = 9 & it . 57 = 5 & it . 58 = 0 & it . 59 = 15 & it . 60 = 14 & it . 61 = 2 & it . 62 = 3 & it . 63 = 12 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 4 & b₁ . 1 = 11 & b₁ . 2 = 2 & b₁ . 3 = 14 & b₁ . 4 = 15 & b₁ . 5 = 0 & b₁ . 6 = 8 & b₁ . 7 = 13 & b₁ . 8 = 3 & b₁ . 9 = 12 & b₁ . 10 = 9 & b₁ . 11 = 7 & b₁ . 12 = 5 & b₁ . 13 = 10 & b₁ . 14 = 6 & b₁ . 15 = 1 & b₁ . 16 = 13 & b₁ . 17 = 0 & b₁ . 18 = 11 & b₁ . 19 = 7 & b₁ . 20 = 4 & b₁ . 21 = 9 & b₁ . 22 = 1 & b₁ . 23 = 10 & b₁ . 24 = 14 & b₁ . 25 = 3 & b₁ . 26 = 5 & b₁ . 27 = 12 & b₁ . 28 = 2 & b₁ . 29 = 15 & b₁ . 30 = 8 & b₁ . 31 = 6 & b₁ . 32 = 1 & b₁ . 33 = 4 & b₁ . 34 = 11 & b₁ . 35 = 13 & b₁ . 36 = 12 & b₁ . 37 = 3 & b₁ . 38 = 7 & b₁ . 39 = 14 & b₁ . 40 = 10 & b₁ . 41 = 15 & b₁ . 42 = 6 & b₁ . 43 = 8 & b₁ . 44 = 0 & b₁ . 45 = 5 & b₁ . 46 = 9 & b₁ . 47 = 2 & b₁ . 48 = 6 & b₁ . 49 = 11 & b₁ . 50 = 13 & b₁ . 51 = 8 & b₁ . 52 = 1 & b₁ . 53 = 4 & b₁ . 54 = 10 & b₁ . 55 = 7 & b₁ . 56 = 9 & b₁ . 57 = 5 & b₁ . 58 = 0 & b₁ . 59 = 15 & b₁ . 60 = 14 & b₁ . 61 = 2 & b₁ . 62 = 3 & b₁ . 63 = 12 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 4 & b₁ . 1 = 11 & b₁ . 2 = 2 & b₁ . 3 = 14 & b₁ . 4 = 15 & b₁ . 5 = 0 & b₁ . 6 = 8 & b₁ . 7 = 13 & b₁ . 8 = 3 & b₁ . 9 = 12 & b₁ . 10 = 9 & b₁ . 11 = 7 & b₁ . 12 = 5 & b₁ . 13 = 10 & b₁ . 14 = 6 & b₁ . 15 = 1 & b₁ . 16 = 13 & b₁ . 17 = 0 & b₁ . 18 = 11 & b₁ . 19 = 7 & b₁ . 20 = 4 & b₁ . 21 = 9 & b₁ . 22 = 1 & b₁ . 23 = 10 & b₁ . 24 = 14 & b₁ . 25 = 3 & b₁ . 26 = 5 & b₁ . 27 = 12 & b₁ . 28 = 2 & b₁ . 29 = 15 & b₁ . 30 = 8 & b₁ . 31 = 6 & b₁ . 32 = 1 & b₁ . 33 = 4 & b₁ . 34 = 11 & b₁ . 35 = 13 & b₁ . 36 = 12 & b₁ . 37 = 3 & b₁ . 38 = 7 & b₁ . 39 = 14 & b₁ . 40 = 10 & b₁ . 41 = 15 & b₁ . 42 = 6 & b₁ . 43 = 8 & b₁ . 44 = 0 & b₁ . 45 = 5 & b₁ . 46 = 9 & b₁ . 47 = 2 & b₁ . 48 = 6 & b₁ . 49 = 11 & b₁ . 50 = 13 & b₁ . 51 = 8 & b₁ . 52 = 1 & b₁ . 53 = 4 & b₁ . 54 = 10 & b₁ . 55 = 7 & b₁ . 56 = 9 & b₁ . 57 = 5 & b₁ . 58 = 0 & b₁ . 59 = 15 & b₁ . 60 = 14 & b₁ . 61 = 2 & b₁ . 62 = 3 & b₁ . 63 = 12 & b₂ . 0 = 4 & b₂ . 1 = 11 & b₂ . 2 = 2 & b₂ . 3 = 14 & b₂ . 4 = 15 & b₂ . 5 = 0 & b₂ . 6 = 8 & b₂ . 7 = 13 & b₂ . 8 = 3 & b₂ . 9 = 12 & b₂ . 10 = 9 & b₂ . 11 = 7 & b₂ . 12 = 5 & b₂ . 13 = 10 & b₂ . 14 = 6 & b₂ . 15 = 1 & b₂ . 16 = 13 & b₂ . 17 = 0 & b₂ . 18 = 11 & b₂ . 19 = 7 & b₂ . 20 = 4 & b₂ . 21 = 9 & b₂ . 22 = 1 & b₂ . 23 = 10 & b₂ . 24 = 14 & b₂ . 25 = 3 & b₂ . 26 = 5 & b₂ . 27 = 12 & b₂ . 28 = 2 & b₂ . 29 = 15 & b₂ . 30 = 8 & b₂ . 31 = 6 & b₂ . 32 = 1 & b₂ . 33 = 4 & b₂ . 34 = 11 & b₂ . 35 = 13 & b₂ . 36 = 12 & b₂ . 37 = 3 & b₂ . 38 = 7 & b₂ . 39 = 14 & b₂ . 40 = 10 & b₂ . 41 = 15 & b₂ . 42 = 6 & b₂ . 43 = 8 & b₂ . 44 = 0 & b₂ . 45 = 5 & b₂ . 46 = 9 & b₂ . 47 = 2 & b₂ . 48 = 6 & b₂ . 49 = 11 & b₂ . 50 = 13 & b₂ . 51 = 8 & b₂ . 52 = 1 & b₂ . 53 = 4 & b₂ . 54 = 10 & b₂ . 55 = 7 & b₂ . 56 = 9 & b₂ . 57 = 5 & b₂ . 58 = 0 & b₂ . 59 = 15 & b₂ . 60 = 14 & b₂ . 61 = 2 & b₂ . 62 = 3 & b₂ . 63 = 12 holds
b₁ = b₂ by Lm4;

end;

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

definition

func DES-SBOX8 -> Function of 64,16 means :: DESCIP_1:def 13
( it . 0 = 13 & it . 1 = 2 & it . 2 = 8 & it . 3 = 4 & it . 4 = 6 & it . 5 = 15 & it . 6 = 11 & it . 7 = 1 & it . 8 = 10 & it . 9 = 9 & it . 10 = 3 & it . 11 = 14 & it . 12 = 5 & it . 13 = 0 & it . 14 = 12 & it . 15 = 7 & it . 16 = 1 & it . 17 = 15 & it . 18 = 13 & it . 19 = 8 & it . 20 = 10 & it . 21 = 3 & it . 22 = 7 & it . 23 = 4 & it . 24 = 12 & it . 25 = 5 & it . 26 = 5 & it . 27 = 11 & it . 28 = 0 & it . 29 = 14 & it . 30 = 9 & it . 31 = 2 & it . 32 = 7 & it . 33 = 11 & it . 34 = 4 & it . 35 = 1 & it . 36 = 9 & it . 37 = 12 & it . 38 = 14 & it . 39 = 2 & it . 40 = 0 & it . 41 = 6 & it . 42 = 10 & it . 43 = 13 & it . 44 = 15 & it . 45 = 3 & it . 46 = 5 & it . 47 = 8 & it . 48 = 2 & it . 49 = 1 & it . 50 = 14 & it . 51 = 7 & it . 52 = 4 & it . 53 = 10 & it . 54 = 8 & it . 55 = 13 & it . 56 = 15 & it . 57 = 12 & it . 58 = 9 & it . 59 = 0 & it . 60 = 3 & it . 61 = 5 & it . 62 = 6 & it . 63 = 11 );

existence
ex b₁ being Function of 64,16 st
( b₁ . 0 = 13 & b₁ . 1 = 2 & b₁ . 2 = 8 & b₁ . 3 = 4 & b₁ . 4 = 6 & b₁ . 5 = 15 & b₁ . 6 = 11 & b₁ . 7 = 1 & b₁ . 8 = 10 & b₁ . 9 = 9 & b₁ . 10 = 3 & b₁ . 11 = 14 & b₁ . 12 = 5 & b₁ . 13 = 0 & b₁ . 14 = 12 & b₁ . 15 = 7 & b₁ . 16 = 1 & b₁ . 17 = 15 & b₁ . 18 = 13 & b₁ . 19 = 8 & b₁ . 20 = 10 & b₁ . 21 = 3 & b₁ . 22 = 7 & b₁ . 23 = 4 & b₁ . 24 = 12 & b₁ . 25 = 5 & b₁ . 26 = 5 & b₁ . 27 = 11 & b₁ . 28 = 0 & b₁ . 29 = 14 & b₁ . 30 = 9 & b₁ . 31 = 2 & b₁ . 32 = 7 & b₁ . 33 = 11 & b₁ . 34 = 4 & b₁ . 35 = 1 & b₁ . 36 = 9 & b₁ . 37 = 12 & b₁ . 38 = 14 & b₁ . 39 = 2 & b₁ . 40 = 0 & b₁ . 41 = 6 & b₁ . 42 = 10 & b₁ . 43 = 13 & b₁ . 44 = 15 & b₁ . 45 = 3 & b₁ . 46 = 5 & b₁ . 47 = 8 & b₁ . 48 = 2 & b₁ . 49 = 1 & b₁ . 50 = 14 & b₁ . 51 = 7 & b₁ . 52 = 4 & b₁ . 53 = 10 & b₁ . 54 = 8 & b₁ . 55 = 13 & b₁ . 56 = 15 & b₁ . 57 = 12 & b₁ . 58 = 9 & b₁ . 59 = 0 & b₁ . 60 = 3 & b₁ . 61 = 5 & b₁ . 62 = 6 & b₁ . 63 = 11 ) by Th27, Lm3;
uniqueness
for b₁, b₂ being Function of 64,16 st b₁ . 0 = 13 & b₁ . 1 = 2 & b₁ . 2 = 8 & b₁ . 3 = 4 & b₁ . 4 = 6 & b₁ . 5 = 15 & b₁ . 6 = 11 & b₁ . 7 = 1 & b₁ . 8 = 10 & b₁ . 9 = 9 & b₁ . 10 = 3 & b₁ . 11 = 14 & b₁ . 12 = 5 & b₁ . 13 = 0 & b₁ . 14 = 12 & b₁ . 15 = 7 & b₁ . 16 = 1 & b₁ . 17 = 15 & b₁ . 18 = 13 & b₁ . 19 = 8 & b₁ . 20 = 10 & b₁ . 21 = 3 & b₁ . 22 = 7 & b₁ . 23 = 4 & b₁ . 24 = 12 & b₁ . 25 = 5 & b₁ . 26 = 5 & b₁ . 27 = 11 & b₁ . 28 = 0 & b₁ . 29 = 14 & b₁ . 30 = 9 & b₁ . 31 = 2 & b₁ . 32 = 7 & b₁ . 33 = 11 & b₁ . 34 = 4 & b₁ . 35 = 1 & b₁ . 36 = 9 & b₁ . 37 = 12 & b₁ . 38 = 14 & b₁ . 39 = 2 & b₁ . 40 = 0 & b₁ . 41 = 6 & b₁ . 42 = 10 & b₁ . 43 = 13 & b₁ . 44 = 15 & b₁ . 45 = 3 & b₁ . 46 = 5 & b₁ . 47 = 8 & b₁ . 48 = 2 & b₁ . 49 = 1 & b₁ . 50 = 14 & b₁ . 51 = 7 & b₁ . 52 = 4 & b₁ . 53 = 10 & b₁ . 54 = 8 & b₁ . 55 = 13 & b₁ . 56 = 15 & b₁ . 57 = 12 & b₁ . 58 = 9 & b₁ . 59 = 0 & b₁ . 60 = 3 & b₁ . 61 = 5 & b₁ . 62 = 6 & b₁ . 63 = 11 & b₂ . 0 = 13 & b₂ . 1 = 2 & b₂ . 2 = 8 & b₂ . 3 = 4 & b₂ . 4 = 6 & b₂ . 5 = 15 & b₂ . 6 = 11 & b₂ . 7 = 1 & b₂ . 8 = 10 & b₂ . 9 = 9 & b₂ . 10 = 3 & b₂ . 11 = 14 & b₂ . 12 = 5 & b₂ . 13 = 0 & b₂ . 14 = 12 & b₂ . 15 = 7 & b₂ . 16 = 1 & b₂ . 17 = 15 & b₂ . 18 = 13 & b₂ . 19 = 8 & b₂ . 20 = 10 & b₂ . 21 = 3 & b₂ . 22 = 7 & b₂ . 23 = 4 & b₂ . 24 = 12 & b₂ . 25 = 5 & b₂ . 26 = 5 & b₂ . 27 = 11 & b₂ . 28 = 0 & b₂ . 29 = 14 & b₂ . 30 = 9 & b₂ . 31 = 2 & b₂ . 32 = 7 & b₂ . 33 = 11 & b₂ . 34 = 4 & b₂ . 35 = 1 & b₂ . 36 = 9 & b₂ . 37 = 12 & b₂ . 38 = 14 & b₂ . 39 = 2 & b₂ . 40 = 0 & b₂ . 41 = 6 & b₂ . 42 = 10 & b₂ . 43 = 13 & b₂ . 44 = 15 & b₂ . 45 = 3 & b₂ . 46 = 5 & b₂ . 47 = 8 & b₂ . 48 = 2 & b₂ . 49 = 1 & b₂ . 50 = 14 & b₂ . 51 = 7 & b₂ . 52 = 4 & b₂ . 53 = 10 & b₂ . 54 = 8 & b₂ . 55 = 13 & b₂ . 56 = 15 & b₂ . 57 = 12 & b₂ . 58 = 9 & b₂ . 59 = 0 & b₂ . 60 = 3 & b₂ . 61 = 5 & b₂ . 62 = 6 & b₂ . 63 = 11 holds
b₁ = b₂ by Lm4;

end;

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

definition

let r be Element of 64 -tuples_on BOOLEAN;

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

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

proof end;

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

proof end;

end;

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

definition

func DES-PIP -> Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) means :Def15: :: DESCIP_1:def 15
for i being Element of 64 -tuples_on BOOLEAN holds it . i = DES-IP i;

existence
ex b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) st
for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IP i

proof end;

uniqueness
for b₁, b₂ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) st ( for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IP i ) & ( for i being Element of 64 -tuples_on BOOLEAN holds b₂ . i = DES-IP i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines DES-PIP DESCIP_1:def 15 :
for b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) holds
( b₁ = DES-PIP iff for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IP i );

definition

let r be Element of 64 -tuples_on BOOLEAN;

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

existence
ex b₁ being Element of 64 -tuples_on BOOLEAN st
( 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 )

proof end;

uniqueness
for b₁, b₂ being Element of 64 -tuples_on BOOLEAN st 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 & 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 holds
b₁ = b₂

proof end;

end;

:: 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 ) );

definition

func DES-PIPINV -> Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) means :Def17: :: DESCIP_1:def 17
for i being Element of 64 -tuples_on BOOLEAN holds it . i = DES-IPINV i;

existence
ex b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) st
for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IPINV i

proof end;

uniqueness
for b₁, b₂ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) st ( for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IPINV i ) & ( for i being Element of 64 -tuples_on BOOLEAN holds b₂ . i = DES-IPINV i ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines DES-PIPINV DESCIP_1:def 17 :
for b₁ being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) holds
( b₁ = DES-PIPINV iff for i being Element of 64 -tuples_on BOOLEAN holds b₁ . i = DES-IPINV i );

Lm5: for x being Element of 64 -tuples_on BOOLEAN holds DES-IPINV (DES-IP x) = x

proof end;

Lm6: for x being Element of 64 -tuples_on BOOLEAN holds DES-IP (DES-IPINV x) = x

proof end;

Lm7: DES-PIPINV * DES-PIP = id (64 -tuples_on BOOLEAN)

proof end;

Lm8: DES-PIP * DES-PIPINV = id (64 -tuples_on BOOLEAN)

proof end;

registration

cluster DES-PIP -> bijective ;

coherence
DES-PIP is bijective by Lm7, Lm8, FUNCT_2:23;

end;

registration

cluster DES-PIPINV -> bijective ;

correctness
coherence
DES-PIPINV is bijective ;
by Lm7, Lm8, FUNCT_2:23;

end;

theorem :: DESCIP_1:28

DES-PIPINV = DES-PIP " by Lm7, FUNCT_2:60;

definition

let r be Element of 32 -tuples_on BOOLEAN;

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

existence
ex b₁ being Element of 48 -tuples_on BOOLEAN st
( 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 )

proof end;

uniqueness
for b₁, b₂ being Element of 48 -tuples_on BOOLEAN st 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 & 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 holds
b₁ = b₂

proof end;

end;

:: 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 ) );

definition

let r be Element of 32 -tuples_on BOOLEAN;

func DES-P r -> Element of 32 -tuples_on BOOLEAN means :: DESCIP_1:def 19
( it . 1 = r . 16 & it . 2 = r . 7 & it . 3 = r . 20 & it . 4 = r . 21 & it . 5 = r . 29 & it . 6 = r . 12 & it . 7 = r . 28 & it . 8 = r . 17 & it . 9 = r . 1 & it . 10 = r . 15 & it . 11 = r . 23 & it . 12 = r . 26 & it . 13 = r . 5 & it . 14 = r . 18 & it . 15 = r . 31 & it . 16 = r . 10 & it . 17 = r . 2 & it . 18 = r . 8 & it . 19 = r . 24 & it . 20 = r . 14 & it . 21 = r . 32 & it . 22 = r . 27 & it . 23 = r . 3 & it . 24 = r . 9 & it . 25 = r . 19 & it . 26 = r . 13 & it . 27 = r . 30 & it . 28 = r . 6 & it . 29 = r . 22 & it . 30 = r . 11 & it . 31 = r . 4 & it . 32 = r . 25 );

existence
ex b₁ being Element of 32 -tuples_on BOOLEAN st
( b₁ . 1 = r . 16 & b₁ . 2 = r . 7 & b₁ . 3 = r . 20 & b₁ . 4 = r . 21 & b₁ . 5 = r . 29 & b₁ . 6 = r . 12 & b₁ . 7 = r . 28 & b₁ . 8 = r . 17 & b₁ . 9 = r . 1 & b₁ . 10 = r . 15 & b₁ . 11 = r . 23 & b₁ . 12 = r . 26 & b₁ . 13 = r . 5 & b₁ . 14 = r . 18 & b₁ . 15 = r . 31 & b₁ . 16 = r . 10 & b₁ . 17 = r . 2 & b₁ . 18 = r . 8 & b₁ . 19 = r . 24 & b₁ . 20 = r . 14 & b₁ . 21 = r . 32 & b₁ . 22 = r . 27 & b₁ . 23 = r . 3 & b₁ . 24 = r . 9 & b₁ . 25 = r . 19 & b₁ . 26 = r . 13 & b₁ . 27 = r . 30 & b₁ . 28 = r . 6 & b₁ . 29 = r . 22 & b₁ . 30 = r . 11 & b₁ . 31 = r . 4 & b₁ . 32 = r . 25 )

proof end;

uniqueness
for b₁, b₂ being Element of 32 -tuples_on BOOLEAN st b₁ . 1 = r . 16 & b₁ . 2 = r . 7 & b₁ . 3 = r . 20 & b₁ . 4 = r . 21 & b₁ . 5 = r . 29 & b₁ . 6 = r . 12 & b₁ . 7 = r . 28 & b₁ . 8 = r . 17 & b₁ . 9 = r . 1 & b₁ . 10 = r . 15 & b₁ . 11 = r . 23 & b₁ . 12 = r . 26 & b₁ . 13 = r . 5 & b₁ . 14 = r . 18 & b₁ . 15 = r . 31 & b₁ . 16 = r . 10 & b₁ . 17 = r . 2 & b₁ . 18 = r . 8 & b₁ . 19 = r . 24 & b₁ . 20 = r . 14 & b₁ . 21 = r . 32 & b₁ . 22 = r . 27 & b₁ . 23 = r . 3 & b₁ . 24 = r . 9 & b₁ . 25 = r . 19 & b₁ . 26 = r . 13 & b₁ . 27 = r . 30 & b₁ . 28 = r . 6 & b₁ . 29 = r . 22 & b₁ . 30 = r . 11 & b₁ . 31 = r . 4 & b₁ . 32 = r . 25 & b₂ . 1 = r . 16 & b₂ . 2 = r . 7 & b₂ . 3 = r . 20 & b₂ . 4 = r . 21 & b₂ . 5 = r . 29 & b₂ . 6 = r . 12 & b₂ . 7 = r . 28 & b₂ . 8 = r . 17 & b₂ . 9 = r . 1 & b₂ . 10 = r . 15 & b₂ . 11 = r . 23 & b₂ . 12 = r . 26 & b₂ . 13 = r . 5 & b₂ . 14 = r . 18 & b₂ . 15 = r . 31 & b₂ . 16 = r . 10 & b₂ . 17 = r . 2 & b₂ . 18 = r . 8 & b₂ . 19 = r . 24 & b₂ . 20 = r . 14 & b₂ . 21 = r . 32 & b₂ . 22 = r . 27 & b₂ . 23 = r . 3 & b₂ . 24 = r . 9 & b₂ . 25 = r . 19 & b₂ . 26 = r . 13 & b₂ . 27 = r . 30 & b₂ . 28 = r . 6 & b₂ . 29 = r . 22 & b₂ . 30 = r . 11 & b₂ . 31 = r . 4 & b₂ . 32 = r . 25 holds
b₁ = b₂

proof end;

end;

:: deftheorem defines DES-P DESCIP_1:def 19 :
for r, b₂ being Element of 32 -tuples_on BOOLEAN holds
( b₂ = DES-P r iff ( b₂ . 1 = r . 16 & b₂ . 2 = r . 7 & b₂ . 3 = r . 20 & b₂ . 4 = r . 21 & b₂ . 5 = r . 29 & b₂ . 6 = r . 12 & b₂ . 7 = r . 28 & b₂ . 8 = r . 17 & b₂ . 9 = r . 1 & b₂ . 10 = r . 15 & b₂ . 11 = r . 23 & b₂ . 12 = r . 26 & b₂ . 13 = r . 5 & b₂ . 14 = r . 18 & b₂ . 15 = r . 31 & b₂ . 16 = r . 10 & b₂ . 17 = r . 2 & b₂ . 18 = r . 8 & b₂ . 19 = r . 24 & b₂ . 20 = r . 14 & b₂ . 21 = r . 32 & b₂ . 22 = r . 27 & b₂ . 23 = r . 3 & b₂ . 24 = r . 9 & b₂ . 25 = r . 19 & b₂ . 26 = r . 13 & b₂ . 27 = r . 30 & b₂ . 28 = r . 6 & b₂ . 29 = r . 22 & b₂ . 30 = r . 11 & b₂ . 31 = r . 4 & b₂ . 32 = r . 25 ) );

definition

let r be Element of 48 -tuples_on BOOLEAN;

func DES-DIV8 r -> Element of 8 -tuples_on (6 -tuples_on BOOLEAN) means :Def20: :: DESCIP_1:def 20
( it . 1 = Op-Left (r,6) & it . 2 = Op-Left ((Op-Right (r,6)),6) & it . 3 = Op-Left ((Op-Right (r,12)),6) & it . 4 = Op-Left ((Op-Right (r,18)),6) & it . 5 = Op-Left ((Op-Right (r,24)),6) & it . 6 = Op-Left ((Op-Right (r,30)),6) & it . 7 = Op-Left ((Op-Right (r,36)),6) & it . 8 = Op-Right (r,42) );

existence
ex b₁ being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) st
( b₁ . 1 = Op-Left (r,6) & b₁ . 2 = Op-Left ((Op-Right (r,6)),6) & b₁ . 3 = Op-Left ((Op-Right (r,12)),6) & b₁ . 4 = Op-Left ((Op-Right (r,18)),6) & b₁ . 5 = Op-Left ((Op-Right (r,24)),6) & b₁ . 6 = Op-Left ((Op-Right (r,30)),6) & b₁ . 7 = Op-Left ((Op-Right (r,36)),6) & b₁ . 8 = Op-Right (r,42) )

proof end;

uniqueness
for b₁, b₂ being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) st b₁ . 1 = Op-Left (r,6) & b₁ . 2 = Op-Left ((Op-Right (r,6)),6) & b₁ . 3 = Op-Left ((Op-Right (r,12)),6) & b₁ . 4 = Op-Left ((Op-Right (r,18)),6) & b₁ . 5 = Op-Left ((Op-Right (r,24)),6) & b₁ . 6 = Op-Left ((Op-Right (r,30)),6) & b₁ . 7 = Op-Left ((Op-Right (r,36)),6) & b₁ . 8 = Op-Right (r,42) & b₂ . 1 = Op-Left (r,6) & b₂ . 2 = Op-Left ((Op-Right (r,6)),6) & b₂ . 3 = Op-Left ((Op-Right (r,12)),6) & b₂ . 4 = Op-Left ((Op-Right (r,18)),6) & b₂ . 5 = Op-Left ((Op-Right (r,24)),6) & b₂ . 6 = Op-Left ((Op-Right (r,30)),6) & b₂ . 7 = Op-Left ((Op-Right (r,36)),6) & b₂ . 8 = Op-Right (r,42) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines DES-DIV8 DESCIP_1:def 20 :
for r being Element of 48 -tuples_on BOOLEAN
for b₂ being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) holds
( b₂ = DES-DIV8 r iff ( b₂ . 1 = Op-Left (r,6) & b₂ . 2 = Op-Left ((Op-Right (r,6)),6) & b₂ . 3 = Op-Left ((Op-Right (r,12)),6) & b₂ . 4 = Op-Left ((Op-Right (r,18)),6) & b₂ . 5 = Op-Left ((Op-Right (r,24)),6) & b₂ . 6 = Op-Left ((Op-Right (r,30)),6) & b₂ . 7 = Op-Left ((Op-Right (r,36)),6) & b₂ . 8 = Op-Right (r,42) ) );

theorem Th29: :: DESCIP_1:29

for r being Element of 48 -tuples_on BOOLEAN ex s1, s2, s3, s4, s5, s6, s7, s8 being Element of 6 -tuples_on BOOLEAN st
( s1 = (DES-DIV8 r) . 1 & s2 = (DES-DIV8 r) . 2 & s3 = (DES-DIV8 r) . 3 & s4 = (DES-DIV8 r) . 4 & s5 = (DES-DIV8 r) . 5 & s6 = (DES-DIV8 r) . 6 & s7 = (DES-DIV8 r) . 7 & s8 = (DES-DIV8 r) . 8 & r = ((((((s1 ^ s2) ^ s3) ^ s4) ^ s5) ^ s6) ^ s7) ^ s8 )

proof end;

Lm9: for n being Nat
for b being Element of BOOLEAN holds n * b <= n

proof end;

definition

let t be Element of 6 -tuples_on BOOLEAN;

func B6toN64 t -> Element of Segm 64 equals :: DESCIP_1:def 21
(((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5));

coherence
(((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5)) is Element of Segm 64

proof end;

end;

:: deftheorem defines B6toN64 DESCIP_1:def 21 :
for t being Element of 6 -tuples_on BOOLEAN holds B6toN64 t = (((((32 * (t . 1)) + (16 * (t . 6))) + (8 * (t . 2))) + (4 * (t . 3))) + (2 * (t . 4))) + (1 * (t . 5));

definition

let a be Element of 16;

func N16toB4 a -> Tuple of 4, BOOLEAN equals :: DESCIP_1:def 22
<*FALSE,FALSE,FALSE,FALSE*> if a = 0
<*FALSE,FALSE,FALSE,TRUE*> if a = 1
<*FALSE,FALSE,TRUE,FALSE*> if a = 2
<*FALSE,FALSE,TRUE,TRUE*> if a = 3
<*FALSE,TRUE,FALSE,FALSE*> if a = 4
<*FALSE,TRUE,FALSE,TRUE*> if a = 5
<*FALSE,TRUE,TRUE,FALSE*> if a = 6
<*FALSE,TRUE,TRUE,TRUE*> if a = 7
<*TRUE,FALSE,FALSE,FALSE*> if a = 8
<*TRUE,FALSE,FALSE,TRUE*> if a = 9
<*TRUE,FALSE,TRUE,FALSE*> if a = 10
<*TRUE,FALSE,TRUE,TRUE*> if a = 11
<*TRUE,TRUE,FALSE,FALSE*> if a = 12
<*TRUE,TRUE,FALSE,TRUE*> if a = 13
<*TRUE,TRUE,TRUE,FALSE*> if a = 15
<*TRUE,TRUE,TRUE,TRUE*> if a = 16
;

coherence
( ( a = 0 implies <*FALSE,FALSE,FALSE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 1 implies <*FALSE,FALSE,FALSE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 2 implies <*FALSE,FALSE,TRUE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 3 implies <*FALSE,FALSE,TRUE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 4 implies <*FALSE,TRUE,FALSE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 5 implies <*FALSE,TRUE,FALSE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 6 implies <*FALSE,TRUE,TRUE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 7 implies <*FALSE,TRUE,TRUE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 8 implies <*TRUE,FALSE,FALSE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 9 implies <*TRUE,FALSE,FALSE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 10 implies <*TRUE,FALSE,TRUE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 11 implies <*TRUE,FALSE,TRUE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 12 implies <*TRUE,TRUE,FALSE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 13 implies <*TRUE,TRUE,FALSE,TRUE*> is Tuple of 4, BOOLEAN ) & ( a = 15 implies <*TRUE,TRUE,TRUE,FALSE*> is Tuple of 4, BOOLEAN ) & ( a = 16 implies <*TRUE,TRUE,TRUE,TRUE*> is Tuple of 4, BOOLEAN ) ) ;
consistency
for b₁ being Tuple of 4, BOOLEAN holds
( ( a = 0 & a = 1 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,FALSE,FALSE,TRUE*> ) ) & ( a = 0 & a = 2 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,FALSE,TRUE,FALSE*> ) ) & ( a = 0 & a = 3 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 0 & a = 4 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 0 & a = 5 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 0 & a = 6 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 0 & a = 7 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 0 & a = 8 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 0 & a = 9 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 0 & a = 10 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 0 & a = 11 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 0 & a = 12 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 0 & a = 13 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 0 & a = 15 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 0 & a = 16 implies ( b₁ = <*FALSE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 1 & a = 2 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,FALSE,TRUE,FALSE*> ) ) & ( a = 1 & a = 3 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 1 & a = 4 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 1 & a = 5 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 1 & a = 6 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 1 & a = 7 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 1 & a = 8 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 1 & a = 9 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 1 & a = 10 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 1 & a = 11 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 1 & a = 12 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 1 & a = 13 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 1 & a = 15 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 1 & a = 16 implies ( b₁ = <*FALSE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 2 & a = 3 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 2 & a = 4 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 2 & a = 5 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 2 & a = 6 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 2 & a = 7 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 2 & a = 8 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 2 & a = 9 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 2 & a = 10 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 2 & a = 11 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 2 & a = 12 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 2 & a = 13 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 2 & a = 15 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 2 & a = 16 implies ( b₁ = <*FALSE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 3 & a = 4 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 3 & a = 5 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 3 & a = 6 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 3 & a = 7 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 3 & a = 8 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 3 & a = 9 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 3 & a = 10 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 3 & a = 11 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 3 & a = 12 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 3 & a = 13 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 3 & a = 15 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 3 & a = 16 implies ( b₁ = <*FALSE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 4 & a = 5 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 4 & a = 6 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 4 & a = 7 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 4 & a = 8 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 4 & a = 9 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 4 & a = 10 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 4 & a = 11 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 4 & a = 12 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 4 & a = 13 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 4 & a = 15 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 4 & a = 16 implies ( b₁ = <*FALSE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 5 & a = 6 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 5 & a = 7 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 5 & a = 8 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 5 & a = 9 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 5 & a = 10 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 5 & a = 11 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 5 & a = 12 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 5 & a = 13 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 5 & a = 15 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 5 & a = 16 implies ( b₁ = <*FALSE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 6 & a = 7 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 6 & a = 8 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 6 & a = 9 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 6 & a = 10 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 6 & a = 11 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 6 & a = 12 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 6 & a = 13 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 6 & a = 15 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 6 & a = 16 implies ( b₁ = <*FALSE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 7 & a = 8 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 7 & a = 9 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 7 & a = 10 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 7 & a = 11 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 7 & a = 12 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 7 & a = 13 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 7 & a = 15 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 7 & a = 16 implies ( b₁ = <*FALSE,TRUE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 8 & a = 9 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 8 & a = 10 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 8 & a = 11 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 8 & a = 12 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 8 & a = 13 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 8 & a = 15 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 8 & a = 16 implies ( b₁ = <*TRUE,FALSE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 9 & a = 10 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 9 & a = 11 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 9 & a = 12 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 9 & a = 13 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 9 & a = 15 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 9 & a = 16 implies ( b₁ = <*TRUE,FALSE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 10 & a = 11 implies ( b₁ = <*TRUE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 10 & a = 12 implies ( b₁ = <*TRUE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 10 & a = 13 implies ( b₁ = <*TRUE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 10 & a = 15 implies ( b₁ = <*TRUE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 10 & a = 16 implies ( b₁ = <*TRUE,FALSE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 11 & a = 12 implies ( b₁ = <*TRUE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 11 & a = 13 implies ( b₁ = <*TRUE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 11 & a = 15 implies ( b₁ = <*TRUE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 11 & a = 16 implies ( b₁ = <*TRUE,FALSE,TRUE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 12 & a = 13 implies ( b₁ = <*TRUE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 12 & a = 15 implies ( b₁ = <*TRUE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 12 & a = 16 implies ( b₁ = <*TRUE,TRUE,FALSE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 13 & a = 15 implies ( b₁ = <*TRUE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 13 & a = 16 implies ( b₁ = <*TRUE,TRUE,FALSE,TRUE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 15 & a = 16 implies ( b₁ = <*TRUE,TRUE,TRUE,FALSE*> iff b₁ = <*TRUE,TRUE,TRUE,TRUE*> ) ) ) ;

end;

:: deftheorem defines N16toB4 DESCIP_1:def 22 :
for a being Element of 16 holds
( ( a = 0 implies N16toB4 a = <*FALSE,FALSE,FALSE,FALSE*> ) & ( a = 1 implies N16toB4 a = <*FALSE,FALSE,FALSE,TRUE*> ) & ( a = 2 implies N16toB4 a = <*FALSE,FALSE,TRUE,FALSE*> ) & ( a = 3 implies N16toB4 a = <*FALSE,FALSE,TRUE,TRUE*> ) & ( a = 4 implies N16toB4 a = <*FALSE,TRUE,FALSE,FALSE*> ) & ( a = 5 implies N16toB4 a = <*FALSE,TRUE,FALSE,TRUE*> ) & ( a = 6 implies N16toB4 a = <*FALSE,TRUE,TRUE,FALSE*> ) & ( a = 7 implies N16toB4 a = <*FALSE,TRUE,TRUE,TRUE*> ) & ( a = 8 implies N16toB4 a = <*TRUE,FALSE,FALSE,FALSE*> ) & ( a = 9 implies N16toB4 a = <*TRUE,FALSE,FALSE,TRUE*> ) & ( a = 10 implies N16toB4 a = <*TRUE,FALSE,TRUE,FALSE*> ) & ( a = 11 implies N16toB4 a = <*TRUE,FALSE,TRUE,TRUE*> ) & ( a = 12 implies N16toB4 a = <*TRUE,TRUE,FALSE,FALSE*> ) & ( a = 13 implies N16toB4 a = <*TRUE,TRUE,FALSE,TRUE*> ) & ( a = 15 implies N16toB4 a = <*TRUE,TRUE,TRUE,FALSE*> ) & ( a = 16 implies N16toB4 a = <*TRUE,TRUE,TRUE,TRUE*> ) );

definition

let R be Element of 32 -tuples_on BOOLEAN;
let RKey be Element of 48 -tuples_on BOOLEAN;

func DES-F (R,RKey) -> Element of 32 -tuples_on BOOLEAN means :: DESCIP_1:def 23
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 & it = DES-P C32 );

existence
ex b₁ being Element of 32 -tuples_on BOOLEAN 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 )

proof end;

uniqueness
for b₁, b₂ being Element of 32 -tuples_on BOOLEAN st 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 ) & 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 ) holds
b₁ = b₂ ;

end;

:: 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 ) );

definition

func DES-FFUNC -> Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) means :: DESCIP_1:def 24
for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds it . z = DES-F ((z `1),(z `2));

existence
ex b₁ being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) st
for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b₁ . z = DES-F ((z `1),(z `2))

proof end;

uniqueness
for b₁, b₂ being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) st ( for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b₁ . z = DES-F ((z `1),(z `2)) ) & ( for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b₂ . z = DES-F ((z `1),(z `2)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines DES-FFUNC DESCIP_1:def 24 :
for b₁ being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) holds
( b₁ = DES-FFUNC iff for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b₁ . z = DES-F ((z `1),(z `2)) );

definition

let r be Element of 64 -tuples_on BOOLEAN;

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

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

proof end;

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

proof end;

end;

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

definition

let r be Element of 56 -tuples_on BOOLEAN;

func DES-PC2 r -> Element of 48 -tuples_on BOOLEAN means :: DESCIP_1:def 26
( it . 1 = r . 14 & it . 2 = r . 17 & it . 3 = r . 11 & it . 4 = r . 24 & it . 5 = r . 1 & it . 6 = r . 5 & it . 7 = r . 3 & it . 8 = r . 28 & it . 9 = r . 15 & it . 10 = r . 6 & it . 11 = r . 21 & it . 12 = r . 10 & it . 13 = r . 23 & it . 14 = r . 19 & it . 15 = r . 12 & it . 16 = r . 4 & it . 17 = r . 26 & it . 18 = r . 8 & it . 19 = r . 16 & it . 20 = r . 7 & it . 21 = r . 27 & it . 22 = r . 20 & it . 23 = r . 13 & it . 24 = r . 2 & it . 25 = r . 41 & it . 26 = r . 52 & it . 27 = r . 31 & it . 28 = r . 37 & it . 29 = r . 47 & it . 30 = r . 55 & it . 31 = r . 30 & it . 32 = r . 40 & it . 33 = r . 51 & it . 34 = r . 45 & it . 35 = r . 33 & it . 36 = r . 48 & it . 37 = r . 44 & it . 38 = r . 49 & it . 39 = r . 39 & it . 40 = r . 56 & it . 41 = r . 34 & it . 42 = r . 53 & it . 43 = r . 46 & it . 44 = r . 42 & it . 45 = r . 50 & it . 46 = r . 36 & it . 47 = r . 29 & it . 48 = r . 32 );

existence
ex b₁ being Element of 48 -tuples_on BOOLEAN st
( b₁ . 1 = r . 14 & b₁ . 2 = r . 17 & b₁ . 3 = r . 11 & b₁ . 4 = r . 24 & b₁ . 5 = r . 1 & b₁ . 6 = r . 5 & b₁ . 7 = r . 3 & b₁ . 8 = r . 28 & b₁ . 9 = r . 15 & b₁ . 10 = r . 6 & b₁ . 11 = r . 21 & b₁ . 12 = r . 10 & b₁ . 13 = r . 23 & b₁ . 14 = r . 19 & b₁ . 15 = r . 12 & b₁ . 16 = r . 4 & b₁ . 17 = r . 26 & b₁ . 18 = r . 8 & b₁ . 19 = r . 16 & b₁ . 20 = r . 7 & b₁ . 21 = r . 27 & b₁ . 22 = r . 20 & b₁ . 23 = r . 13 & b₁ . 24 = r . 2 & b₁ . 25 = r . 41 & b₁ . 26 = r . 52 & b₁ . 27 = r . 31 & b₁ . 28 = r . 37 & b₁ . 29 = r . 47 & b₁ . 30 = r . 55 & b₁ . 31 = r . 30 & b₁ . 32 = r . 40 & b₁ . 33 = r . 51 & b₁ . 34 = r . 45 & b₁ . 35 = r . 33 & b₁ . 36 = r . 48 & b₁ . 37 = r . 44 & b₁ . 38 = r . 49 & b₁ . 39 = r . 39 & b₁ . 40 = r . 56 & b₁ . 41 = r . 34 & b₁ . 42 = r . 53 & b₁ . 43 = r . 46 & b₁ . 44 = r . 42 & b₁ . 45 = r . 50 & b₁ . 46 = r . 36 & b₁ . 47 = r . 29 & b₁ . 48 = r . 32 )

proof end;

uniqueness
for b₁, b₂ being Element of 48 -tuples_on BOOLEAN st b₁ . 1 = r . 14 & b₁ . 2 = r . 17 & b₁ . 3 = r . 11 & b₁ . 4 = r . 24 & b₁ . 5 = r . 1 & b₁ . 6 = r . 5 & b₁ . 7 = r . 3 & b₁ . 8 = r . 28 & b₁ . 9 = r . 15 & b₁ . 10 = r . 6 & b₁ . 11 = r . 21 & b₁ . 12 = r . 10 & b₁ . 13 = r . 23 & b₁ . 14 = r . 19 & b₁ . 15 = r . 12 & b₁ . 16 = r . 4 & b₁ . 17 = r . 26 & b₁ . 18 = r . 8 & b₁ . 19 = r . 16 & b₁ . 20 = r . 7 & b₁ . 21 = r . 27 & b₁ . 22 = r . 20 & b₁ . 23 = r . 13 & b₁ . 24 = r . 2 & b₁ . 25 = r . 41 & b₁ . 26 = r . 52 & b₁ . 27 = r . 31 & b₁ . 28 = r . 37 & b₁ . 29 = r . 47 & b₁ . 30 = r . 55 & b₁ . 31 = r . 30 & b₁ . 32 = r . 40 & b₁ . 33 = r . 51 & b₁ . 34 = r . 45 & b₁ . 35 = r . 33 & b₁ . 36 = r . 48 & b₁ . 37 = r . 44 & b₁ . 38 = r . 49 & b₁ . 39 = r . 39 & b₁ . 40 = r . 56 & b₁ . 41 = r . 34 & b₁ . 42 = r . 53 & b₁ . 43 = r . 46 & b₁ . 44 = r . 42 & b₁ . 45 = r . 50 & b₁ . 46 = r . 36 & b₁ . 47 = r . 29 & b₁ . 48 = r . 32 & b₂ . 1 = r . 14 & b₂ . 2 = r . 17 & b₂ . 3 = r . 11 & b₂ . 4 = r . 24 & b₂ . 5 = r . 1 & b₂ . 6 = r . 5 & b₂ . 7 = r . 3 & b₂ . 8 = r . 28 & b₂ . 9 = r . 15 & b₂ . 10 = r . 6 & b₂ . 11 = r . 21 & b₂ . 12 = r . 10 & b₂ . 13 = r . 23 & b₂ . 14 = r . 19 & b₂ . 15 = r . 12 & b₂ . 16 = r . 4 & b₂ . 17 = r . 26 & b₂ . 18 = r . 8 & b₂ . 19 = r . 16 & b₂ . 20 = r . 7 & b₂ . 21 = r . 27 & b₂ . 22 = r . 20 & b₂ . 23 = r . 13 & b₂ . 24 = r . 2 & b₂ . 25 = r . 41 & b₂ . 26 = r . 52 & b₂ . 27 = r . 31 & b₂ . 28 = r . 37 & b₂ . 29 = r . 47 & b₂ . 30 = r . 55 & b₂ . 31 = r . 30 & b₂ . 32 = r . 40 & b₂ . 33 = r . 51 & b₂ . 34 = r . 45 & b₂ . 35 = r . 33 & b₂ . 36 = r . 48 & b₂ . 37 = r . 44 & b₂ . 38 = r . 49 & b₂ . 39 = r . 39 & b₂ . 40 = r . 56 & b₂ . 41 = r . 34 & b₂ . 42 = r . 53 & b₂ . 43 = r . 46 & b₂ . 44 = r . 42 & b₂ . 45 = r . 50 & b₂ . 46 = r . 36 & b₂ . 47 = r . 29 & b₂ . 48 = r . 32 holds
b₁ = b₂

proof end;

end;

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

definition

func bitshift_DES -> FinSequence of NAT means :: DESCIP_1:def 27
( it is 16 -element & it . 1 = 1 & it . 2 = 1 & it . 3 = 2 & it . 4 = 2 & it . 5 = 2 & it . 6 = 2 & it . 7 = 2 & it . 8 = 2 & it . 9 = 1 & it . 10 = 2 & it . 11 = 2 & it . 12 = 2 & it . 13 = 2 & it . 14 = 2 & it . 15 = 2 & it . 16 = 1 );

existence
ex b₁ being FinSequence of NAT st
( b₁ is 16 -element & b₁ . 1 = 1 & b₁ . 2 = 1 & b₁ . 3 = 2 & b₁ . 4 = 2 & b₁ . 5 = 2 & b₁ . 6 = 2 & b₁ . 7 = 2 & b₁ . 8 = 2 & b₁ . 9 = 1 & b₁ . 10 = 2 & b₁ . 11 = 2 & b₁ . 12 = 2 & b₁ . 13 = 2 & b₁ . 14 = 2 & b₁ . 15 = 2 & b₁ . 16 = 1 ) by Th21;
uniqueness
for b₁, b₂ being FinSequence of NAT st b₁ is 16 -element & b₁ . 1 = 1 & b₁ . 2 = 1 & b₁ . 3 = 2 & b₁ . 4 = 2 & b₁ . 5 = 2 & b₁ . 6 = 2 & b₁ . 7 = 2 & b₁ . 8 = 2 & b₁ . 9 = 1 & b₁ . 10 = 2 & b₁ . 11 = 2 & b₁ . 12 = 2 & b₁ . 13 = 2 & b₁ . 14 = 2 & b₁ . 15 = 2 & b₁ . 16 = 1 & b₂ is 16 -element & b₂ . 1 = 1 & b₂ . 2 = 1 & b₂ . 3 = 2 & b₂ . 4 = 2 & b₂ . 5 = 2 & b₂ . 6 = 2 & b₂ . 7 = 2 & b₂ . 8 = 2 & b₂ . 9 = 1 & b₂ . 10 = 2 & b₂ . 11 = 2 & b₂ . 12 = 2 & b₂ . 13 = 2 & b₂ . 14 = 2 & b₂ . 15 = 2 & b₂ . 16 = 1 holds
b₁ = b₂

proof end;

end;

:: deftheorem defines bitshift_DES DESCIP_1:def 27 :
for b₁ being FinSequence of NAT holds
( b₁ = bitshift_DES iff ( b₁ is 16 -element & b₁ . 1 = 1 & b₁ . 2 = 1 & b₁ . 3 = 2 & b₁ . 4 = 2 & b₁ . 5 = 2 & b₁ . 6 = 2 & b₁ . 7 = 2 & b₁ . 8 = 2 & b₁ . 9 = 1 & b₁ . 10 = 2 & b₁ . 11 = 2 & b₁ . 12 = 2 & b₁ . 13 = 2 & b₁ . 14 = 2 & b₁ . 15 = 2 & b₁ . 16 = 1 ) );

definition

let Key be Element of 64 -tuples_on BOOLEAN;

func DES-KS Key -> Element of 16 -tuples_on (48 -tuples_on BOOLEAN) means :: DESCIP_1:def 28
ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( it . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) );

existence
ex b₁ being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₁ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) st ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₁ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) & ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₂ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines DES-KS DESCIP_1:def 28 :
for Key being Element of 64 -tuples_on BOOLEAN
for b₂ being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) holds
( b₂ = DES-KS Key iff ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₂ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) );

Lm10: for m, n, k being non zero Element of NAT
for RK being Element of k -tuples_on (m -tuples_on BOOLEAN)
for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )

proof end;

definition

let n, m, k be non zero Element of NAT ;
let RK be Element of k -tuples_on (m -tuples_on BOOLEAN);
let F be Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN);
let IP be Permutation of ((2 * n) -tuples_on BOOLEAN);
let M be Element of (2 * n) -tuples_on BOOLEAN;

func DES-like-CoDec (M,F,IP,RK) -> Element of (2 * n) -tuples_on BOOLEAN means :Def29: :: DESCIP_1:def 29
ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & it = (IP ") . ((R . k) ^ (L . k)) );

existence
ex b₁ being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & b₁ = (IP ") . ((R . k) ^ (L . k)) ) by Lm10;
uniqueness
for b₁, b₂ being Element of (2 * n) -tuples_on BOOLEAN st ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & b₁ = (IP ") . ((R . k) ^ (L . k)) ) & ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & b₂ = (IP ") . ((R . k) ^ (L . k)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def29 defines DES-like-CoDec DESCIP_1:def 29 :
for n, m, k being non zero Element of NAT
for RK being Element of k -tuples_on (m -tuples_on BOOLEAN)
for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M, b₈ being Element of (2 * n) -tuples_on BOOLEAN holds
( b₈ = DES-like-CoDec (M,F,IP,RK) iff ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & b₈ = (IP ") . ((R . k) ^ (L . k)) ) );

theorem Th30: :: DESCIP_1:30

for n, m, k being non zero Element of NAT
for RK being Element of k -tuples_on (m -tuples_on BOOLEAN)
for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN holds DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M

proof end;

definition

let RK be Element of 16 -tuples_on (48 -tuples_on BOOLEAN);
let F be Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN);
let IP be Permutation of (64 -tuples_on BOOLEAN);
let M be Element of 64 -tuples_on BOOLEAN;

func DES-CoDec (M,F,IP,RK) -> Element of 64 -tuples_on BOOLEAN means :Def30: :: DESCIP_1:def 30
ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & it = DES-like-CoDec (MX,F,IPX,RK) );

existence
ex b₁ being Element of 64 -tuples_on BOOLEAN ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & b₁ = DES-like-CoDec (MX,F,IPX,RK) )

proof end;

uniqueness
for b₁, b₂ being Element of 64 -tuples_on BOOLEAN st ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & b₁ = DES-like-CoDec (MX,F,IPX,RK) ) & ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & b₂ = DES-like-CoDec (MX,F,IPX,RK) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def30 defines DES-CoDec DESCIP_1:def 30 :
for RK being Element of 16 -tuples_on (48 -tuples_on BOOLEAN)
for F being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN)
for IP being Permutation of (64 -tuples_on BOOLEAN)
for M, b₅ being Element of 64 -tuples_on BOOLEAN holds
( b₅ = DES-CoDec (M,F,IP,RK) iff ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & b₅ = DES-like-CoDec (MX,F,IPX,RK) ) );

theorem Th31: :: DESCIP_1:31

for RK being Element of 16 -tuples_on (48 -tuples_on BOOLEAN)
for F being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN)
for IP being Permutation of (64 -tuples_on BOOLEAN)
for M being Element of 64 -tuples_on BOOLEAN holds DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M

proof end;

definition

let plaintext, secretkey be Element of 64 -tuples_on BOOLEAN;

func DES-ENC (plaintext,secretkey) -> Element of 64 -tuples_on BOOLEAN equals :: DESCIP_1:def 31
DES-CoDec (plaintext,DES-FFUNC,DES-PIP,(DES-KS secretkey));

correctness
coherence
DES-CoDec (plaintext,DES-FFUNC,DES-PIP,(DES-KS secretkey)) is Element of 64 -tuples_on BOOLEAN;
;

end;

:: deftheorem defines DES-ENC DESCIP_1:def 31 :
for plaintext, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-ENC (plaintext,secretkey) = DES-CoDec (plaintext,DES-FFUNC,DES-PIP,(DES-KS secretkey));

definition

let ciphertext, secretkey be Element of 64 -tuples_on BOOLEAN;

func DES-DEC (ciphertext,secretkey) -> Element of 64 -tuples_on BOOLEAN equals :: DESCIP_1:def 32
DES-CoDec (ciphertext,DES-FFUNC,DES-PIP,(Rev (DES-KS secretkey)));

correctness
coherence
DES-CoDec (ciphertext,DES-FFUNC,DES-PIP,(Rev (DES-KS secretkey))) is Element of 64 -tuples_on BOOLEAN;
;

end;

:: deftheorem defines DES-DEC DESCIP_1:def 32 :
for ciphertext, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-DEC (ciphertext,secretkey) = DES-CoDec (ciphertext,DES-FFUNC,DES-PIP,(Rev (DES-KS secretkey)));

theorem :: DESCIP_1:32

for message, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-DEC ((DES-ENC (message,secretkey)),secretkey) = message by Th31;