:: 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 b1 being FinSequence of D st
( len b1 = len s & ( for i being Nat st i in Seg (len s) holds
b1 . i = s . ((((i - 1) + n) mod (len s)) + 1) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = len s & ( for i being Nat st i in Seg (len s) holds
b1 . i = s . ((((i - 1) + n) mod (len s)) + 1) ) & len b2 = len s & ( for i being Nat st i in Seg (len s) holds
b2 . i = s . ((((i - 1) + n) mod (len s)) + 1) ) holds
b1 = b2
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 b4 being FinSequence of D holds
( b4 = Op-Shift (s,n) iff ( len b4 = len s & ( for i being Nat st i in Seg (len s) holds
b4 . 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 b1 being Element of n -tuples_on BOOLEAN holds b1 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 b1 being Element of n -tuples_on BOOLEAN holds
( b1 = Op-XOR (t,) iff for i being Nat st i in Seg n holds
b1 . 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, b4 being Element of n -tuples_on BOOLEAN holds
( b4 = Op-XOR (s,t) iff for i being Nat st i in Seg n holds
b4 . 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{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> Element of F1(), F6() -> Element of F2(), F7() -> Element of F3(), F8() -> Element of F4(), P1[ object , object , object , object , object , object , object , object , object ] } :
ex f being sequence of F1() ex g being sequence of F2() ex h being sequence of F3() ex i being sequence of F4() st
( f . 0 = F5() & g . 0 = F6() & h . 0 = F7() & i . 0 = F8() & ( for n being Element of NAT holds P1[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 F1()
for y being Element of F2()
for z being Element of F3()
for w being Element of F4() ex x1 being Element of F1() ex y1 being Element of F2() ex z1 being Element of F3() ex w1 being Element of F4() st P1[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 b1 being Function of (Segm n),(Seg n) st b1 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 b1 being NtoSEG Function of (Segm n),(Seg n) holds b1 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 b1 being Function of 64,16 st
( b1 . 0 = 14 & b1 . 1 = 4 & b1 . 2 = 13 & b1 . 3 = 1 & b1 . 4 = 2 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 8 & b1 . 8 = 3 & b1 . 9 = 10 & b1 . 10 = 6 & b1 . 11 = 12 & b1 . 12 = 5 & b1 . 13 = 9 & b1 . 14 = 0 & b1 . 15 = 7 & b1 . 16 = 0 & b1 . 17 = 15 & b1 . 18 = 7 & b1 . 19 = 4 & b1 . 20 = 14 & b1 . 21 = 2 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 10 & b1 . 25 = 6 & b1 . 26 = 12 & b1 . 27 = 11 & b1 . 28 = 9 & b1 . 29 = 5 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 4 & b1 . 33 = 1 & b1 . 34 = 14 & b1 . 35 = 8 & b1 . 36 = 13 & b1 . 37 = 6 & b1 . 38 = 2 & b1 . 39 = 11 & b1 . 40 = 15 & b1 . 41 = 12 & b1 . 42 = 9 & b1 . 43 = 7 & b1 . 44 = 3 & b1 . 45 = 10 & b1 . 46 = 5 & b1 . 47 = 0 & b1 . 48 = 15 & b1 . 49 = 12 & b1 . 50 = 8 & b1 . 51 = 2 & b1 . 52 = 4 & b1 . 53 = 9 & b1 . 54 = 1 & b1 . 55 = 7 & b1 . 56 = 5 & b1 . 57 = 11 & b1 . 58 = 3 & b1 . 59 = 14 & b1 . 60 = 10 & b1 . 61 = 0 & b1 . 62 = 6 & b1 . 63 = 13 ) by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 14 & b1 . 1 = 4 & b1 . 2 = 13 & b1 . 3 = 1 & b1 . 4 = 2 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 8 & b1 . 8 = 3 & b1 . 9 = 10 & b1 . 10 = 6 & b1 . 11 = 12 & b1 . 12 = 5 & b1 . 13 = 9 & b1 . 14 = 0 & b1 . 15 = 7 & b1 . 16 = 0 & b1 . 17 = 15 & b1 . 18 = 7 & b1 . 19 = 4 & b1 . 20 = 14 & b1 . 21 = 2 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 10 & b1 . 25 = 6 & b1 . 26 = 12 & b1 . 27 = 11 & b1 . 28 = 9 & b1 . 29 = 5 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 4 & b1 . 33 = 1 & b1 . 34 = 14 & b1 . 35 = 8 & b1 . 36 = 13 & b1 . 37 = 6 & b1 . 38 = 2 & b1 . 39 = 11 & b1 . 40 = 15 & b1 . 41 = 12 & b1 . 42 = 9 & b1 . 43 = 7 & b1 . 44 = 3 & b1 . 45 = 10 & b1 . 46 = 5 & b1 . 47 = 0 & b1 . 48 = 15 & b1 . 49 = 12 & b1 . 50 = 8 & b1 . 51 = 2 & b1 . 52 = 4 & b1 . 53 = 9 & b1 . 54 = 1 & b1 . 55 = 7 & b1 . 56 = 5 & b1 . 57 = 11 & b1 . 58 = 3 & b1 . 59 = 14 & b1 . 60 = 10 & b1 . 61 = 0 & b1 . 62 = 6 & b1 . 63 = 13 & b2 . 0 = 14 & b2 . 1 = 4 & b2 . 2 = 13 & b2 . 3 = 1 & b2 . 4 = 2 & b2 . 5 = 15 & b2 . 6 = 11 & b2 . 7 = 8 & b2 . 8 = 3 & b2 . 9 = 10 & b2 . 10 = 6 & b2 . 11 = 12 & b2 . 12 = 5 & b2 . 13 = 9 & b2 . 14 = 0 & b2 . 15 = 7 & b2 . 16 = 0 & b2 . 17 = 15 & b2 . 18 = 7 & b2 . 19 = 4 & b2 . 20 = 14 & b2 . 21 = 2 & b2 . 22 = 13 & b2 . 23 = 1 & b2 . 24 = 10 & b2 . 25 = 6 & b2 . 26 = 12 & b2 . 27 = 11 & b2 . 28 = 9 & b2 . 29 = 5 & b2 . 30 = 3 & b2 . 31 = 8 & b2 . 32 = 4 & b2 . 33 = 1 & b2 . 34 = 14 & b2 . 35 = 8 & b2 . 36 = 13 & b2 . 37 = 6 & b2 . 38 = 2 & b2 . 39 = 11 & b2 . 40 = 15 & b2 . 41 = 12 & b2 . 42 = 9 & b2 . 43 = 7 & b2 . 44 = 3 & b2 . 45 = 10 & b2 . 46 = 5 & b2 . 47 = 0 & b2 . 48 = 15 & b2 . 49 = 12 & b2 . 50 = 8 & b2 . 51 = 2 & b2 . 52 = 4 & b2 . 53 = 9 & b2 . 54 = 1 & b2 . 55 = 7 & b2 . 56 = 5 & b2 . 57 = 11 & b2 . 58 = 3 & b2 . 59 = 14 & b2 . 60 = 10 & b2 . 61 = 0 & b2 . 62 = 6 & b2 . 63 = 13 holds
b1 = b2 by Lm4;
end;

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

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

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

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

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

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

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

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

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

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

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

:: deftheorem Def17 defines DES-PIPINV DESCIP_1:def 17 :
for b1 being Function of (64 -tuples_on BOOLEAN),(64 -tuples_on BOOLEAN) holds
( b1 = DES-PIPINV iff for i being Element of 64 -tuples_on BOOLEAN holds b1 . 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 b1 being Element of 48 -tuples_on BOOLEAN st
( b1 . 1 = r . 32 & b1 . 2 = r . 1 & b1 . 3 = r . 2 & b1 . 4 = r . 3 & b1 . 5 = r . 4 & b1 . 6 = r . 5 & b1 . 7 = r . 4 & b1 . 8 = r . 5 & b1 . 9 = r . 6 & b1 . 10 = r . 7 & b1 . 11 = r . 8 & b1 . 12 = r . 9 & b1 . 13 = r . 8 & b1 . 14 = r . 9 & b1 . 15 = r . 10 & b1 . 16 = r . 11 & b1 . 17 = r . 12 & b1 . 18 = r . 13 & b1 . 19 = r . 12 & b1 . 20 = r . 13 & b1 . 21 = r . 14 & b1 . 22 = r . 15 & b1 . 23 = r . 16 & b1 . 24 = r . 17 & b1 . 25 = r . 16 & b1 . 26 = r . 17 & b1 . 27 = r . 18 & b1 . 28 = r . 19 & b1 . 29 = r . 20 & b1 . 30 = r . 21 & b1 . 31 = r . 20 & b1 . 32 = r . 21 & b1 . 33 = r . 22 & b1 . 34 = r . 23 & b1 . 35 = r . 24 & b1 . 36 = r . 25 & b1 . 37 = r . 24 & b1 . 38 = r . 25 & b1 . 39 = r . 26 & b1 . 40 = r . 27 & b1 . 41 = r . 28 & b1 . 42 = r . 29 & b1 . 43 = r . 28 & b1 . 44 = r . 29 & b1 . 45 = r . 30 & b1 . 46 = r . 31 & b1 . 47 = r . 32 & b1 . 48 = r . 1 )
proof end;
uniqueness
for b1, b2 being Element of 48 -tuples_on BOOLEAN st b1 . 1 = r . 32 & b1 . 2 = r . 1 & b1 . 3 = r . 2 & b1 . 4 = r . 3 & b1 . 5 = r . 4 & b1 . 6 = r . 5 & b1 . 7 = r . 4 & b1 . 8 = r . 5 & b1 . 9 = r . 6 & b1 . 10 = r . 7 & b1 . 11 = r . 8 & b1 . 12 = r . 9 & b1 . 13 = r . 8 & b1 . 14 = r . 9 & b1 . 15 = r . 10 & b1 . 16 = r . 11 & b1 . 17 = r . 12 & b1 . 18 = r . 13 & b1 . 19 = r . 12 & b1 . 20 = r . 13 & b1 . 21 = r . 14 & b1 . 22 = r . 15 & b1 . 23 = r . 16 & b1 . 24 = r . 17 & b1 . 25 = r . 16 & b1 . 26 = r . 17 & b1 . 27 = r . 18 & b1 . 28 = r . 19 & b1 . 29 = r . 20 & b1 . 30 = r . 21 & b1 . 31 = r . 20 & b1 . 32 = r . 21 & b1 . 33 = r . 22 & b1 . 34 = r . 23 & b1 . 35 = r . 24 & b1 . 36 = r . 25 & b1 . 37 = r . 24 & b1 . 38 = r . 25 & b1 . 39 = r . 26 & b1 . 40 = r . 27 & b1 . 41 = r . 28 & b1 . 42 = r . 29 & b1 . 43 = r . 28 & b1 . 44 = r . 29 & b1 . 45 = r . 30 & b1 . 46 = r . 31 & b1 . 47 = r . 32 & b1 . 48 = r . 1 & b2 . 1 = r . 32 & b2 . 2 = r . 1 & b2 . 3 = r . 2 & b2 . 4 = r . 3 & b2 . 5 = r . 4 & b2 . 6 = r . 5 & b2 . 7 = r . 4 & b2 . 8 = r . 5 & b2 . 9 = r . 6 & b2 . 10 = r . 7 & b2 . 11 = r . 8 & b2 . 12 = r . 9 & b2 . 13 = r . 8 & b2 . 14 = r . 9 & b2 . 15 = r . 10 & b2 . 16 = r . 11 & b2 . 17 = r . 12 & b2 . 18 = r . 13 & b2 . 19 = r . 12 & b2 . 20 = r . 13 & b2 . 21 = r . 14 & b2 . 22 = r . 15 & b2 . 23 = r . 16 & b2 . 24 = r . 17 & b2 . 25 = r . 16 & b2 . 26 = r . 17 & b2 . 27 = r . 18 & b2 . 28 = r . 19 & b2 . 29 = r . 20 & b2 . 30 = r . 21 & b2 . 31 = r . 20 & b2 . 32 = r . 21 & b2 . 33 = r . 22 & b2 . 34 = r . 23 & b2 . 35 = r . 24 & b2 . 36 = r . 25 & b2 . 37 = r . 24 & b2 . 38 = r . 25 & b2 . 39 = r . 26 & b2 . 40 = r . 27 & b2 . 41 = r . 28 & b2 . 42 = r . 29 & b2 . 43 = r . 28 & b2 . 44 = r . 29 & b2 . 45 = r . 30 & b2 . 46 = r . 31 & b2 . 47 = r . 32 & b2 . 48 = r . 1 holds
b1 = b2
proof end;
end;

:: deftheorem defines DES-E DESCIP_1:def 18 :
for r being Element of 32 -tuples_on BOOLEAN
for b2 being Element of 48 -tuples_on BOOLEAN holds
( b2 = DES-E r iff ( b2 . 1 = r . 32 & b2 . 2 = r . 1 & b2 . 3 = r . 2 & b2 . 4 = r . 3 & b2 . 5 = r . 4 & b2 . 6 = r . 5 & b2 . 7 = r . 4 & b2 . 8 = r . 5 & b2 . 9 = r . 6 & b2 . 10 = r . 7 & b2 . 11 = r . 8 & b2 . 12 = r . 9 & b2 . 13 = r . 8 & b2 . 14 = r . 9 & b2 . 15 = r . 10 & b2 . 16 = r . 11 & b2 . 17 = r . 12 & b2 . 18 = r . 13 & b2 . 19 = r . 12 & b2 . 20 = r . 13 & b2 . 21 = r . 14 & b2 . 22 = r . 15 & b2 . 23 = r . 16 & b2 . 24 = r . 17 & b2 . 25 = r . 16 & b2 . 26 = r . 17 & b2 . 27 = r . 18 & b2 . 28 = r . 19 & b2 . 29 = r . 20 & b2 . 30 = r . 21 & b2 . 31 = r . 20 & b2 . 32 = r . 21 & b2 . 33 = r . 22 & b2 . 34 = r . 23 & b2 . 35 = r . 24 & b2 . 36 = r . 25 & b2 . 37 = r . 24 & b2 . 38 = r . 25 & b2 . 39 = r . 26 & b2 . 40 = r . 27 & b2 . 41 = r . 28 & b2 . 42 = r . 29 & b2 . 43 = r . 28 & b2 . 44 = r . 29 & b2 . 45 = r . 30 & b2 . 46 = r . 31 & b2 . 47 = r . 32 & b2 . 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 b1 being Element of 32 -tuples_on BOOLEAN st
( b1 . 1 = r . 16 & b1 . 2 = r . 7 & b1 . 3 = r . 20 & b1 . 4 = r . 21 & b1 . 5 = r . 29 & b1 . 6 = r . 12 & b1 . 7 = r . 28 & b1 . 8 = r . 17 & b1 . 9 = r . 1 & b1 . 10 = r . 15 & b1 . 11 = r . 23 & b1 . 12 = r . 26 & b1 . 13 = r . 5 & b1 . 14 = r . 18 & b1 . 15 = r . 31 & b1 . 16 = r . 10 & b1 . 17 = r . 2 & b1 . 18 = r . 8 & b1 . 19 = r . 24 & b1 . 20 = r . 14 & b1 . 21 = r . 32 & b1 . 22 = r . 27 & b1 . 23 = r . 3 & b1 . 24 = r . 9 & b1 . 25 = r . 19 & b1 . 26 = r . 13 & b1 . 27 = r . 30 & b1 . 28 = r . 6 & b1 . 29 = r . 22 & b1 . 30 = r . 11 & b1 . 31 = r . 4 & b1 . 32 = r . 25 )
proof end;
uniqueness
for b1, b2 being Element of 32 -tuples_on BOOLEAN st b1 . 1 = r . 16 & b1 . 2 = r . 7 & b1 . 3 = r . 20 & b1 . 4 = r . 21 & b1 . 5 = r . 29 & b1 . 6 = r . 12 & b1 . 7 = r . 28 & b1 . 8 = r . 17 & b1 . 9 = r . 1 & b1 . 10 = r . 15 & b1 . 11 = r . 23 & b1 . 12 = r . 26 & b1 . 13 = r . 5 & b1 . 14 = r . 18 & b1 . 15 = r . 31 & b1 . 16 = r . 10 & b1 . 17 = r . 2 & b1 . 18 = r . 8 & b1 . 19 = r . 24 & b1 . 20 = r . 14 & b1 . 21 = r . 32 & b1 . 22 = r . 27 & b1 . 23 = r . 3 & b1 . 24 = r . 9 & b1 . 25 = r . 19 & b1 . 26 = r . 13 & b1 . 27 = r . 30 & b1 . 28 = r . 6 & b1 . 29 = r . 22 & b1 . 30 = r . 11 & b1 . 31 = r . 4 & b1 . 32 = r . 25 & b2 . 1 = r . 16 & b2 . 2 = r . 7 & b2 . 3 = r . 20 & b2 . 4 = r . 21 & b2 . 5 = r . 29 & b2 . 6 = r . 12 & b2 . 7 = r . 28 & b2 . 8 = r . 17 & b2 . 9 = r . 1 & b2 . 10 = r . 15 & b2 . 11 = r . 23 & b2 . 12 = r . 26 & b2 . 13 = r . 5 & b2 . 14 = r . 18 & b2 . 15 = r . 31 & b2 . 16 = r . 10 & b2 . 17 = r . 2 & b2 . 18 = r . 8 & b2 . 19 = r . 24 & b2 . 20 = r . 14 & b2 . 21 = r . 32 & b2 . 22 = r . 27 & b2 . 23 = r . 3 & b2 . 24 = r . 9 & b2 . 25 = r . 19 & b2 . 26 = r . 13 & b2 . 27 = r . 30 & b2 . 28 = r . 6 & b2 . 29 = r . 22 & b2 . 30 = r . 11 & b2 . 31 = r . 4 & b2 . 32 = r . 25 holds
b1 = b2
proof end;
end;

:: deftheorem defines DES-P DESCIP_1:def 19 :
for r, b2 being Element of 32 -tuples_on BOOLEAN holds
( b2 = DES-P r iff ( b2 . 1 = r . 16 & b2 . 2 = r . 7 & b2 . 3 = r . 20 & b2 . 4 = r . 21 & b2 . 5 = r . 29 & b2 . 6 = r . 12 & b2 . 7 = r . 28 & b2 . 8 = r . 17 & b2 . 9 = r . 1 & b2 . 10 = r . 15 & b2 . 11 = r . 23 & b2 . 12 = r . 26 & b2 . 13 = r . 5 & b2 . 14 = r . 18 & b2 . 15 = r . 31 & b2 . 16 = r . 10 & b2 . 17 = r . 2 & b2 . 18 = r . 8 & b2 . 19 = r . 24 & b2 . 20 = r . 14 & b2 . 21 = r . 32 & b2 . 22 = r . 27 & b2 . 23 = r . 3 & b2 . 24 = r . 9 & b2 . 25 = r . 19 & b2 . 26 = r . 13 & b2 . 27 = r . 30 & b2 . 28 = r . 6 & b2 . 29 = r . 22 & b2 . 30 = r . 11 & b2 . 31 = r . 4 & b2 . 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 b1 being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) st
( b1 . 1 = Op-Left (r,6) & b1 . 2 = Op-Left ((Op-Right (r,6)),6) & b1 . 3 = Op-Left ((Op-Right (r,12)),6) & b1 . 4 = Op-Left ((Op-Right (r,18)),6) & b1 . 5 = Op-Left ((Op-Right (r,24)),6) & b1 . 6 = Op-Left ((Op-Right (r,30)),6) & b1 . 7 = Op-Left ((Op-Right (r,36)),6) & b1 . 8 = Op-Right (r,42) )
proof end;
uniqueness
for b1, b2 being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) st b1 . 1 = Op-Left (r,6) & b1 . 2 = Op-Left ((Op-Right (r,6)),6) & b1 . 3 = Op-Left ((Op-Right (r,12)),6) & b1 . 4 = Op-Left ((Op-Right (r,18)),6) & b1 . 5 = Op-Left ((Op-Right (r,24)),6) & b1 . 6 = Op-Left ((Op-Right (r,30)),6) & b1 . 7 = Op-Left ((Op-Right (r,36)),6) & b1 . 8 = Op-Right (r,42) & b2 . 1 = Op-Left (r,6) & b2 . 2 = Op-Left ((Op-Right (r,6)),6) & b2 . 3 = Op-Left ((Op-Right (r,12)),6) & b2 . 4 = Op-Left ((Op-Right (r,18)),6) & b2 . 5 = Op-Left ((Op-Right (r,24)),6) & b2 . 6 = Op-Left ((Op-Right (r,30)),6) & b2 . 7 = Op-Left ((Op-Right (r,36)),6) & b2 . 8 = Op-Right (r,42) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines DES-DIV8 DESCIP_1:def 20 :
for r being Element of 48 -tuples_on BOOLEAN
for b2 being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) holds
( b2 = DES-DIV8 r iff ( b2 . 1 = Op-Left (r,6) & b2 . 2 = Op-Left ((Op-Right (r,6)),6) & b2 . 3 = Op-Left ((Op-Right (r,12)),6) & b2 . 4 = Op-Left ((Op-Right (r,18)),6) & b2 . 5 = Op-Left ((Op-Right (r,24)),6) & b2 . 6 = Op-Left ((Op-Right (r,30)),6) & b2 . 7 = Op-Left ((Op-Right (r,36)),6) & b2 . 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 b1 being Tuple of 4, BOOLEAN holds
( ( a = 0 & a = 1 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,FALSE,FALSE,TRUE*> ) ) & ( a = 0 & a = 2 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,FALSE,TRUE,FALSE*> ) ) & ( a = 0 & a = 3 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 0 & a = 4 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 0 & a = 5 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 0 & a = 6 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 0 & a = 7 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 0 & a = 8 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 0 & a = 9 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 0 & a = 10 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 0 & a = 11 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 0 & a = 12 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 0 & a = 13 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 0 & a = 15 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 0 & a = 16 implies ( b1 = <*FALSE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 1 & a = 2 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,FALSE,TRUE,FALSE*> ) ) & ( a = 1 & a = 3 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 1 & a = 4 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 1 & a = 5 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 1 & a = 6 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 1 & a = 7 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 1 & a = 8 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 1 & a = 9 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 1 & a = 10 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 1 & a = 11 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 1 & a = 12 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 1 & a = 13 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 1 & a = 15 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 1 & a = 16 implies ( b1 = <*FALSE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 2 & a = 3 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*FALSE,FALSE,TRUE,TRUE*> ) ) & ( a = 2 & a = 4 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 2 & a = 5 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 2 & a = 6 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 2 & a = 7 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 2 & a = 8 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 2 & a = 9 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 2 & a = 10 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 2 & a = 11 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 2 & a = 12 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 2 & a = 13 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 2 & a = 15 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 2 & a = 16 implies ( b1 = <*FALSE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 3 & a = 4 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*FALSE,TRUE,FALSE,FALSE*> ) ) & ( a = 3 & a = 5 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 3 & a = 6 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 3 & a = 7 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 3 & a = 8 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 3 & a = 9 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 3 & a = 10 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 3 & a = 11 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 3 & a = 12 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 3 & a = 13 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 3 & a = 15 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 3 & a = 16 implies ( b1 = <*FALSE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 4 & a = 5 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,FALSE,TRUE*> ) ) & ( a = 4 & a = 6 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 4 & a = 7 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 4 & a = 8 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 4 & a = 9 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 4 & a = 10 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 4 & a = 11 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 4 & a = 12 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 4 & a = 13 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 4 & a = 15 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 4 & a = 16 implies ( b1 = <*FALSE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 5 & a = 6 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,FALSE*> ) ) & ( a = 5 & a = 7 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 5 & a = 8 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 5 & a = 9 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 5 & a = 10 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 5 & a = 11 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 5 & a = 12 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 5 & a = 13 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 5 & a = 15 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 5 & a = 16 implies ( b1 = <*FALSE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 6 & a = 7 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*FALSE,TRUE,TRUE,TRUE*> ) ) & ( a = 6 & a = 8 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 6 & a = 9 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 6 & a = 10 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 6 & a = 11 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 6 & a = 12 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 6 & a = 13 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 6 & a = 15 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 6 & a = 16 implies ( b1 = <*FALSE,TRUE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 7 & a = 8 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,FALSE*> ) ) & ( a = 7 & a = 9 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 7 & a = 10 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 7 & a = 11 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 7 & a = 12 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 7 & a = 13 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 7 & a = 15 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 7 & a = 16 implies ( b1 = <*FALSE,TRUE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 8 & a = 9 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,FALSE,TRUE*> ) ) & ( a = 8 & a = 10 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 8 & a = 11 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 8 & a = 12 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 8 & a = 13 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 8 & a = 15 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 8 & a = 16 implies ( b1 = <*TRUE,FALSE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 9 & a = 10 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,FALSE*> ) ) & ( a = 9 & a = 11 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 9 & a = 12 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 9 & a = 13 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 9 & a = 15 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 9 & a = 16 implies ( b1 = <*TRUE,FALSE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 10 & a = 11 implies ( b1 = <*TRUE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,FALSE,TRUE,TRUE*> ) ) & ( a = 10 & a = 12 implies ( b1 = <*TRUE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 10 & a = 13 implies ( b1 = <*TRUE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 10 & a = 15 implies ( b1 = <*TRUE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 10 & a = 16 implies ( b1 = <*TRUE,FALSE,TRUE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 11 & a = 12 implies ( b1 = <*TRUE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,FALSE*> ) ) & ( a = 11 & a = 13 implies ( b1 = <*TRUE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 11 & a = 15 implies ( b1 = <*TRUE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 11 & a = 16 implies ( b1 = <*TRUE,FALSE,TRUE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 12 & a = 13 implies ( b1 = <*TRUE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,FALSE,TRUE*> ) ) & ( a = 12 & a = 15 implies ( b1 = <*TRUE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 12 & a = 16 implies ( b1 = <*TRUE,TRUE,FALSE,FALSE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 13 & a = 15 implies ( b1 = <*TRUE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,FALSE*> ) ) & ( a = 13 & a = 16 implies ( b1 = <*TRUE,TRUE,FALSE,TRUE*> iff b1 = <*TRUE,TRUE,TRUE,TRUE*> ) ) & ( a = 15 & a = 16 implies ( b1 = <*TRUE,TRUE,TRUE,FALSE*> iff b1 = <*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 b1 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 & b1 = DES-P C32 )
proof end;
uniqueness
for b1, b2 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 & b1 = 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 & b2 = DES-P C32 ) holds
b1 = b2 ;
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 b3 being Element of 32 -tuples_on BOOLEAN holds
( b3 = 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 & b3 = 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 b1 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 b1 . z = DES-F ((z `1),(z `2))
proof end;
uniqueness
for b1, b2 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 b1 . z = DES-F ((z `1),(z `2)) ) & ( for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b2 . z = DES-F ((z `1),(z `2)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines DES-FFUNC DESCIP_1:def 24 :
for b1 being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN) holds
( b1 = DES-FFUNC iff for z being Element of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):] holds b1 . 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 b1 being Element of 56 -tuples_on BOOLEAN st
( b1 . 1 = r . 57 & b1 . 2 = r . 49 & b1 . 3 = r . 41 & b1 . 4 = r . 33 & b1 . 5 = r . 25 & b1 . 6 = r . 17 & b1 . 7 = r . 9 & b1 . 8 = r . 1 & b1 . 9 = r . 58 & b1 . 10 = r . 50 & b1 . 11 = r . 42 & b1 . 12 = r . 34 & b1 . 13 = r . 26 & b1 . 14 = r . 18 & b1 . 15 = r . 10 & b1 . 16 = r . 2 & b1 . 17 = r . 59 & b1 . 18 = r . 51 & b1 . 19 = r . 43 & b1 . 20 = r . 35 & b1 . 21 = r . 27 & b1 . 22 = r . 19 & b1 . 23 = r . 11 & b1 . 24 = r . 3 & b1 . 25 = r . 60 & b1 . 26 = r . 52 & b1 . 27 = r . 44 & b1 . 28 = r . 36 & b1 . 29 = r . 63 & b1 . 30 = r . 55 & b1 . 31 = r . 47 & b1 . 32 = r . 39 & b1 . 33 = r . 31 & b1 . 34 = r . 23 & b1 . 35 = r . 15 & b1 . 36 = r . 7 & b1 . 37 = r . 62 & b1 . 38 = r . 54 & b1 . 39 = r . 46 & b1 . 40 = r . 38 & b1 . 41 = r . 30 & b1 . 42 = r . 22 & b1 . 43 = r . 14 & b1 . 44 = r . 6 & b1 . 45 = r . 61 & b1 . 46 = r . 53 & b1 . 47 = r . 45 & b1 . 48 = r . 37 & b1 . 49 = r . 29 & b1 . 50 = r . 21 & b1 . 51 = r . 13 & b1 . 52 = r . 5 & b1 . 53 = r . 28 & b1 . 54 = r . 20 & b1 . 55 = r . 12 & b1 . 56 = r . 4 )
proof end;
uniqueness
for b1, b2 being Element of 56 -tuples_on BOOLEAN st b1 . 1 = r . 57 & b1 . 2 = r . 49 & b1 . 3 = r . 41 & b1 . 4 = r . 33 & b1 . 5 = r . 25 & b1 . 6 = r . 17 & b1 . 7 = r . 9 & b1 . 8 = r . 1 & b1 . 9 = r . 58 & b1 . 10 = r . 50 & b1 . 11 = r . 42 & b1 . 12 = r . 34 & b1 . 13 = r . 26 & b1 . 14 = r . 18 & b1 . 15 = r . 10 & b1 . 16 = r . 2 & b1 . 17 = r . 59 & b1 . 18 = r . 51 & b1 . 19 = r . 43 & b1 . 20 = r . 35 & b1 . 21 = r . 27 & b1 . 22 = r . 19 & b1 . 23 = r . 11 & b1 . 24 = r . 3 & b1 . 25 = r . 60 & b1 . 26 = r . 52 & b1 . 27 = r . 44 & b1 . 28 = r . 36 & b1 . 29 = r . 63 & b1 . 30 = r . 55 & b1 . 31 = r . 47 & b1 . 32 = r . 39 & b1 . 33 = r . 31 & b1 . 34 = r . 23 & b1 . 35 = r . 15 & b1 . 36 = r . 7 & b1 . 37 = r . 62 & b1 . 38 = r . 54 & b1 . 39 = r . 46 & b1 . 40 = r . 38 & b1 . 41 = r . 30 & b1 . 42 = r . 22 & b1 . 43 = r . 14 & b1 . 44 = r . 6 & b1 . 45 = r . 61 & b1 . 46 = r . 53 & b1 . 47 = r . 45 & b1 . 48 = r . 37 & b1 . 49 = r . 29 & b1 . 50 = r . 21 & b1 . 51 = r . 13 & b1 . 52 = r . 5 & b1 . 53 = r . 28 & b1 . 54 = r . 20 & b1 . 55 = r . 12 & b1 . 56 = r . 4 & b2 . 1 = r . 57 & b2 . 2 = r . 49 & b2 . 3 = r . 41 & b2 . 4 = r . 33 & b2 . 5 = r . 25 & b2 . 6 = r . 17 & b2 . 7 = r . 9 & b2 . 8 = r . 1 & b2 . 9 = r . 58 & b2 . 10 = r . 50 & b2 . 11 = r . 42 & b2 . 12 = r . 34 & b2 . 13 = r . 26 & b2 . 14 = r . 18 & b2 . 15 = r . 10 & b2 . 16 = r . 2 & b2 . 17 = r . 59 & b2 . 18 = r . 51 & b2 . 19 = r . 43 & b2 . 20 = r . 35 & b2 . 21 = r . 27 & b2 . 22 = r . 19 & b2 . 23 = r . 11 & b2 . 24 = r . 3 & b2 . 25 = r . 60 & b2 . 26 = r . 52 & b2 . 27 = r . 44 & b2 . 28 = r . 36 & b2 . 29 = r . 63 & b2 . 30 = r . 55 & b2 . 31 = r . 47 & b2 . 32 = r . 39 & b2 . 33 = r . 31 & b2 . 34 = r . 23 & b2 . 35 = r . 15 & b2 . 36 = r . 7 & b2 . 37 = r . 62 & b2 . 38 = r . 54 & b2 . 39 = r . 46 & b2 . 40 = r . 38 & b2 . 41 = r . 30 & b2 . 42 = r . 22 & b2 . 43 = r . 14 & b2 . 44 = r . 6 & b2 . 45 = r . 61 & b2 . 46 = r . 53 & b2 . 47 = r . 45 & b2 . 48 = r . 37 & b2 . 49 = r . 29 & b2 . 50 = r . 21 & b2 . 51 = r . 13 & b2 . 52 = r . 5 & b2 . 53 = r . 28 & b2 . 54 = r . 20 & b2 . 55 = r . 12 & b2 . 56 = r . 4 holds
b1 = b2
proof end;
end;

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

:: deftheorem defines DES-PC2 DESCIP_1:def 26 :
for r being Element of 56 -tuples_on BOOLEAN
for b2 being Element of 48 -tuples_on BOOLEAN holds
( b2 = DES-PC2 r iff ( b2 . 1 = r . 14 & b2 . 2 = r . 17 & b2 . 3 = r . 11 & b2 . 4 = r . 24 & b2 . 5 = r . 1 & b2 . 6 = r . 5 & b2 . 7 = r . 3 & b2 . 8 = r . 28 & b2 . 9 = r . 15 & b2 . 10 = r . 6 & b2 . 11 = r . 21 & b2 . 12 = r . 10 & b2 . 13 = r . 23 & b2 . 14 = r . 19 & b2 . 15 = r . 12 & b2 . 16 = r . 4 & b2 . 17 = r . 26 & b2 . 18 = r . 8 & b2 . 19 = r . 16 & b2 . 20 = r . 7 & b2 . 21 = r . 27 & b2 . 22 = r . 20 & b2 . 23 = r . 13 & b2 . 24 = r . 2 & b2 . 25 = r . 41 & b2 . 26 = r . 52 & b2 . 27 = r . 31 & b2 . 28 = r . 37 & b2 . 29 = r . 47 & b2 . 30 = r . 55 & b2 . 31 = r . 30 & b2 . 32 = r . 40 & b2 . 33 = r . 51 & b2 . 34 = r . 45 & b2 . 35 = r . 33 & b2 . 36 = r . 48 & b2 . 37 = r . 44 & b2 . 38 = r . 49 & b2 . 39 = r . 39 & b2 . 40 = r . 56 & b2 . 41 = r . 34 & b2 . 42 = r . 53 & b2 . 43 = r . 46 & b2 . 44 = r . 42 & b2 . 45 = r . 50 & b2 . 46 = r . 36 & b2 . 47 = r . 29 & b2 . 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 b1 being FinSequence of NAT st
( b1 is 16 -element & b1 . 1 = 1 & b1 . 2 = 1 & b1 . 3 = 2 & b1 . 4 = 2 & b1 . 5 = 2 & b1 . 6 = 2 & b1 . 7 = 2 & b1 . 8 = 2 & b1 . 9 = 1 & b1 . 10 = 2 & b1 . 11 = 2 & b1 . 12 = 2 & b1 . 13 = 2 & b1 . 14 = 2 & b1 . 15 = 2 & b1 . 16 = 1 ) by Th21;
uniqueness
for b1, b2 being FinSequence of NAT st b1 is 16 -element & b1 . 1 = 1 & b1 . 2 = 1 & b1 . 3 = 2 & b1 . 4 = 2 & b1 . 5 = 2 & b1 . 6 = 2 & b1 . 7 = 2 & b1 . 8 = 2 & b1 . 9 = 1 & b1 . 10 = 2 & b1 . 11 = 2 & b1 . 12 = 2 & b1 . 13 = 2 & b1 . 14 = 2 & b1 . 15 = 2 & b1 . 16 = 1 & b2 is 16 -element & b2 . 1 = 1 & b2 . 2 = 1 & b2 . 3 = 2 & b2 . 4 = 2 & b2 . 5 = 2 & b2 . 6 = 2 & b2 . 7 = 2 & b2 . 8 = 2 & b2 . 9 = 1 & b2 . 10 = 2 & b2 . 11 = 2 & b2 . 12 = 2 & b2 . 13 = 2 & b2 . 14 = 2 & b2 . 15 = 2 & b2 . 16 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem defines bitshift_DES DESCIP_1:def 27 :
for b1 being FinSequence of NAT holds
( b1 = bitshift_DES iff ( b1 is 16 -element & b1 . 1 = 1 & b1 . 2 = 1 & b1 . 3 = 2 & b1 . 4 = 2 & b1 . 5 = 2 & b1 . 6 = 2 & b1 . 7 = 2 & b1 . 8 = 2 & b1 . 9 = 1 & b1 . 10 = 2 & b1 . 11 = 2 & b1 . 12 = 2 & b1 . 13 = 2 & b1 . 14 = 2 & b1 . 15 = 2 & b1 . 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 b1 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
( b1 . (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 b1, b2 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
( b1 . (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
( b2 . (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
b1 = b2
proof end;
end;

:: deftheorem defines DES-KS DESCIP_1:def 28 :
for Key being Element of 64 -tuples_on BOOLEAN
for b2 being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) holds
( b2 = 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
( b2 . (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 b1 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))))) ) ) & b1 = (IP ") . ((R . k) ^ (L . k)) ) by Lm10;
uniqueness
for b1, b2 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))))) ) ) & b1 = (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))))) ) ) & b2 = (IP ") . ((R . k) ^ (L . k)) ) holds
b1 = b2
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, b8 being Element of (2 * n) -tuples_on BOOLEAN holds
( b8 = 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))))) ) ) & b8 = (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 b1 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 & b1 = DES-like-CoDec (MX,F,IPX,RK) )
proof end;
uniqueness
for b1, b2 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 & b1 = 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 & b2 = DES-like-CoDec (MX,F,IPX,RK) ) holds
b1 = b2 ;
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, b5 being Element of 64 -tuples_on BOOLEAN holds
( b5 = 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 & b5 = 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;