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


begin

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 LM001B: :: DESCIP_1:1
for D being non empty set
for m, n being non empty 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 LM002B: :: DESCIP_1:2
for D being non empty set
for m, n, l being non empty 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 empty 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 SPLR: :: DESCIP_1:3
for D being non empty set
for n being non empty 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 LM003: :: DESCIP_1:4
for s being FinSequence st 1 <= len s holds
len (Op-LeftShift s) = len s
proof end;

theorem LM003A: :: 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 empty 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 LM004: :: DESCIP_1:7
for s being FinSequence holds len (Op-RightShift s) = len s
proof end;

theorem LM004A: :: 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 & len (Op-RightShift s) = len s )
proof end;

theorem :: DESCIP_1:9
for D being non empty set
for n being non empty 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 AS: 1 <= len s ;
func Op-Shift (s,n) -> FinSequence of D means :defShift: :: 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 defShift 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 LM008: :: DESCIP_1:14
for D being non empty set
for n being non empty 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 empty 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;

definition
let n be non empty Element of NAT ;
let s be Element of n -tuples_on NAT;
let i be Nat;
:: original: .
redefine func s . i -> Element of NAT ;
coherence
s . i is Element of NAT
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 empty 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 :defXOR: :: 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;
commutativity
for b1, s, t being Element of n -tuples_on BOOLEAN st ( for i being Nat st i in Seg n holds
b1 . i = (s . i) 'xor' (t . i) ) holds
for i being Nat st i in Seg n holds
b1 . i = (t . i) 'xor' (s . i) ;
end;

:: deftheorem defXOR defines Op-XOR DESCIP_1:def 4 :
for n being non empty 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 empty 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 LM011: :: DESCIP_1:17
for n being non empty 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 empty 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 LC1: :: 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[ set , set , set , set , set , set , set , set , set ] } :
ex f being Function of NAT,F1() ex g being Function of NAT,F2() ex h being Function of NAT,F3() ex i being Function of NAT,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;

Lmseg4: for i, j being Nat st i <= j & j <= i + 3 & not j = i & not j = i + 1 & not j = i + 2 holds
j = i + 3
proof end;

Lmseg8: for i, j being Nat st i <= j & j <= i + 7 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 holds
j = i + 7
proof end;

Lmseg16: for i, j being Nat st i <= j & j <= i + 15 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 holds
j = i + 15
proof end;

Lmseg24: for i, j being Nat st i <= j & j <= i + 23 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 holds
j = i + 23
proof end;

Lmseg32: for i, j being Nat st i <= j & j <= i + 31 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 & not j = i + 23 & not j = i + 24 & not j = i + 25 & not j = i + 26 & not j = i + 27 & not j = i + 28 & not j = i + 29 & not j = i + 30 holds
j = i + 31
proof end;

Lmseg48: for i, j being Nat st i <= j & j <= i + 47 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 & not j = i + 23 & not j = i + 24 & not j = i + 25 & not j = i + 26 & not j = i + 27 & not j = i + 28 & not j = i + 29 & not j = i + 30 & not j = i + 31 & not j = i + 32 & not j = i + 33 & not j = i + 34 & not j = i + 35 & not j = i + 36 & not j = i + 37 & not j = i + 38 & not j = i + 39 & not j = i + 40 & not j = i + 41 & not j = i + 42 & not j = i + 43 & not j = i + 44 & not j = i + 45 & not j = i + 46 holds
j = i + 47
proof end;

Lmseg56: for i, j being Nat st i <= j & j <= i + 55 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 & not j = i + 23 & not j = i + 24 & not j = i + 25 & not j = i + 26 & not j = i + 27 & not j = i + 28 & not j = i + 29 & not j = i + 30 & not j = i + 31 & not j = i + 32 & not j = i + 33 & not j = i + 34 & not j = i + 35 & not j = i + 36 & not j = i + 37 & not j = i + 38 & not j = i + 39 & not j = i + 40 & not j = i + 41 & not j = i + 42 & not j = i + 43 & not j = i + 44 & not j = i + 45 & not j = i + 46 & not j = i + 47 & not j = i + 48 & not j = i + 49 & not j = i + 50 & not j = i + 51 & not j = i + 52 & not j = i + 53 & not j = i + 54 holds
j = i + 55
proof end;

Lmseg64: for i, j being Nat st i <= j & j <= i + 63 & not j = i & not j = i + 1 & not j = i + 2 & not j = i + 3 & not j = i + 4 & not j = i + 5 & not j = i + 6 & not j = i + 7 & not j = i + 8 & not j = i + 9 & not j = i + 10 & not j = i + 11 & not j = i + 12 & not j = i + 13 & not j = i + 14 & not j = i + 15 & not j = i + 16 & not j = i + 17 & not j = i + 18 & not j = i + 19 & not j = i + 20 & not j = i + 21 & not j = i + 22 & not j = i + 23 & not j = i + 24 & not j = i + 25 & not j = i + 26 & not j = i + 27 & not j = i + 28 & not j = i + 29 & not j = i + 30 & not j = i + 31 & not j = i + 32 & not j = i + 33 & not j = i + 34 & not j = i + 35 & not j = i + 36 & not j = i + 37 & not j = i + 38 & not j = i + 39 & not j = i + 40 & not j = i + 41 & not j = i + 42 & not j = i + 43 & not j = i + 44 & not j = i + 45 & not j = i + 46 & not j = i + 47 & not j = i + 48 & not j = i + 49 & not j = i + 50 & not j = i + 51 & not j = i + 52 & not j = i + 53 & not j = i + 54 & not j = i + 55 & not j = i + 56 & not j = i + 57 & not j = i + 58 & not j = i + 59 & not j = i + 60 & not j = i + 61 & not j = i + 62 holds
j = i + 63
proof end;

theorem Lmseg16a: :: DESCIP_1:19
for x being set holds
( not x in Seg 16 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 )
proof end;

theorem Lmseg32a: :: DESCIP_1:20
for x being set holds
( not x in Seg 32 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 )
proof end;

theorem Lmseg48a: :: DESCIP_1:21
for x being set holds
( not x in Seg 48 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 )
proof end;

theorem Lmseg56a: :: DESCIP_1:22
for x being set holds
( not x in Seg 56 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 )
proof end;

theorem Lmseg64a: :: DESCIP_1:23
for x being set holds
( not x in Seg 64 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 or x = 57 or x = 58 or x = 59 or x = 60 or x = 61 or x = 62 or x = 63 or x = 64 )
proof end;

theorem th1: :: DESCIP_1:24
for n being non empty Nat holds n = {0} \/ ((Seg n) \ {n})
proof end;

theorem th3: :: DESCIP_1:25
for n being non empty Nat
for x being set holds
( not x in n or x = 0 or ( x in Seg n & x <> n ) )
proof end;

theorem thel16: :: DESCIP_1:26
for x being set holds
( not x in 16 or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 )
proof end;

theorem thel64: :: DESCIP_1:27
for x being set holds
( not x in 64 or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 or x = 57 or x = 58 or x = 59 or x = 60 or x = 61 or x = 62 or x = 63 )
proof end;

T8: for S being non empty set
for p, q being FinSequence of S st p is 4 -element & q is 4 -element holds
( p ^ q is 8 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = q . 1 & (p ^ q) . 6 = q . 2 & (p ^ q) . 7 = q . 3 & (p ^ q) . 8 = q . 4 )
proof end;

theorem TT8: :: DESCIP_1:28
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;

T16: for S being non empty set
for p, q being FinSequence of S st p is 8 -element & q is 8 -element holds
( p ^ q is 16 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = q . 1 & (p ^ q) . 10 = q . 2 & (p ^ q) . 11 = q . 3 & (p ^ q) . 12 = q . 4 & (p ^ q) . 13 = q . 5 & (p ^ q) . 14 = q . 6 & (p ^ q) . 15 = q . 7 & (p ^ q) . 16 = q . 8 )
proof end;

theorem TT16: :: DESCIP_1:29
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;

T32: for S being non empty set
for p, q being FinSequence of S st p is 16 -element & q is 16 -element holds
( p ^ q is 32 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = p . 9 & (p ^ q) . 10 = p . 10 & (p ^ q) . 11 = p . 11 & (p ^ q) . 12 = p . 12 & (p ^ q) . 13 = p . 13 & (p ^ q) . 14 = p . 14 & (p ^ q) . 15 = p . 15 & (p ^ q) . 16 = p . 16 & (p ^ q) . 17 = q . 1 & (p ^ q) . 18 = q . 2 & (p ^ q) . 19 = q . 3 & (p ^ q) . 20 = q . 4 & (p ^ q) . 21 = q . 5 & (p ^ q) . 22 = q . 6 & (p ^ q) . 23 = q . 7 & (p ^ q) . 24 = q . 8 & (p ^ q) . 25 = q . 9 & (p ^ q) . 26 = q . 10 & (p ^ q) . 27 = q . 11 & (p ^ q) . 28 = q . 12 & (p ^ q) . 29 = q . 13 & (p ^ q) . 30 = q . 14 & (p ^ q) . 31 = q . 15 & (p ^ q) . 32 = q . 16 )
proof end;

theorem TT32: :: DESCIP_1:30
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;

T48: for S being non empty set
for p, q being FinSequence of S st p is 32 -element & q is 16 -element holds
( p ^ q is 48 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = p . 9 & (p ^ q) . 10 = p . 10 & (p ^ q) . 11 = p . 11 & (p ^ q) . 12 = p . 12 & (p ^ q) . 13 = p . 13 & (p ^ q) . 14 = p . 14 & (p ^ q) . 15 = p . 15 & (p ^ q) . 16 = p . 16 & (p ^ q) . 17 = p . 17 & (p ^ q) . 18 = p . 18 & (p ^ q) . 19 = p . 19 & (p ^ q) . 20 = p . 20 & (p ^ q) . 21 = p . 21 & (p ^ q) . 22 = p . 22 & (p ^ q) . 23 = p . 23 & (p ^ q) . 24 = p . 24 & (p ^ q) . 25 = p . 25 & (p ^ q) . 26 = p . 26 & (p ^ q) . 27 = p . 27 & (p ^ q) . 28 = p . 28 & (p ^ q) . 29 = p . 29 & (p ^ q) . 30 = p . 30 & (p ^ q) . 31 = p . 31 & (p ^ q) . 32 = p . 32 & (p ^ q) . 33 = q . 1 & (p ^ q) . 34 = q . 2 & (p ^ q) . 35 = q . 3 & (p ^ q) . 36 = q . 4 & (p ^ q) . 37 = q . 5 & (p ^ q) . 38 = q . 6 & (p ^ q) . 39 = q . 7 & (p ^ q) . 40 = q . 8 & (p ^ q) . 41 = q . 9 & (p ^ q) . 42 = q . 10 & (p ^ q) . 43 = q . 11 & (p ^ q) . 44 = q . 12 & (p ^ q) . 45 = q . 13 & (p ^ q) . 46 = q . 14 & (p ^ q) . 47 = q . 15 & (p ^ q) . 48 = q . 16 )
proof end;

theorem TT48: :: DESCIP_1:31
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;

T56: for S being non empty set
for p, q being FinSequence of S st p is 48 -element & q is 8 -element holds
( p ^ q is 56 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = p . 9 & (p ^ q) . 10 = p . 10 & (p ^ q) . 11 = p . 11 & (p ^ q) . 12 = p . 12 & (p ^ q) . 13 = p . 13 & (p ^ q) . 14 = p . 14 & (p ^ q) . 15 = p . 15 & (p ^ q) . 16 = p . 16 & (p ^ q) . 17 = p . 17 & (p ^ q) . 18 = p . 18 & (p ^ q) . 19 = p . 19 & (p ^ q) . 20 = p . 20 & (p ^ q) . 21 = p . 21 & (p ^ q) . 22 = p . 22 & (p ^ q) . 23 = p . 23 & (p ^ q) . 24 = p . 24 & (p ^ q) . 25 = p . 25 & (p ^ q) . 26 = p . 26 & (p ^ q) . 27 = p . 27 & (p ^ q) . 28 = p . 28 & (p ^ q) . 29 = p . 29 & (p ^ q) . 30 = p . 30 & (p ^ q) . 31 = p . 31 & (p ^ q) . 32 = p . 32 & (p ^ q) . 33 = p . 33 & (p ^ q) . 34 = p . 34 & (p ^ q) . 35 = p . 35 & (p ^ q) . 36 = p . 36 & (p ^ q) . 37 = p . 37 & (p ^ q) . 38 = p . 38 & (p ^ q) . 39 = p . 39 & (p ^ q) . 40 = p . 40 & (p ^ q) . 41 = p . 41 & (p ^ q) . 42 = p . 42 & (p ^ q) . 43 = p . 43 & (p ^ q) . 44 = p . 44 & (p ^ q) . 45 = p . 45 & (p ^ q) . 46 = p . 46 & (p ^ q) . 47 = p . 47 & (p ^ q) . 48 = p . 48 & (p ^ q) . 49 = q . 1 & (p ^ q) . 50 = q . 2 & (p ^ q) . 51 = q . 3 & (p ^ q) . 52 = q . 4 & (p ^ q) . 53 = q . 5 & (p ^ q) . 54 = q . 6 & (p ^ q) . 55 = q . 7 & (p ^ q) . 56 = q . 8 )
proof end;

theorem TT56: :: DESCIP_1:32
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;

T64: for S being non empty set
for p, q being FinSequence of S st p is 32 -element & q is 32 -element holds
( p ^ q is 64 -element & (p ^ q) . 1 = p . 1 & (p ^ q) . 2 = p . 2 & (p ^ q) . 3 = p . 3 & (p ^ q) . 4 = p . 4 & (p ^ q) . 5 = p . 5 & (p ^ q) . 6 = p . 6 & (p ^ q) . 7 = p . 7 & (p ^ q) . 8 = p . 8 & (p ^ q) . 9 = p . 9 & (p ^ q) . 10 = p . 10 & (p ^ q) . 11 = p . 11 & (p ^ q) . 12 = p . 12 & (p ^ q) . 13 = p . 13 & (p ^ q) . 14 = p . 14 & (p ^ q) . 15 = p . 15 & (p ^ q) . 16 = p . 16 & (p ^ q) . 17 = p . 17 & (p ^ q) . 18 = p . 18 & (p ^ q) . 19 = p . 19 & (p ^ q) . 20 = p . 20 & (p ^ q) . 21 = p . 21 & (p ^ q) . 22 = p . 22 & (p ^ q) . 23 = p . 23 & (p ^ q) . 24 = p . 24 & (p ^ q) . 25 = p . 25 & (p ^ q) . 26 = p . 26 & (p ^ q) . 27 = p . 27 & (p ^ q) . 28 = p . 28 & (p ^ q) . 29 = p . 29 & (p ^ q) . 30 = p . 30 & (p ^ q) . 31 = p . 31 & (p ^ q) . 32 = p . 32 & (p ^ q) . 33 = q . 1 & (p ^ q) . 34 = q . 2 & (p ^ q) . 35 = q . 3 & (p ^ q) . 36 = q . 4 & (p ^ q) . 37 = q . 5 & (p ^ q) . 38 = q . 6 & (p ^ q) . 39 = q . 7 & (p ^ q) . 40 = q . 8 & (p ^ q) . 41 = q . 9 & (p ^ q) . 42 = q . 10 & (p ^ q) . 43 = q . 11 & (p ^ q) . 44 = q . 12 & (p ^ q) . 45 = q . 13 & (p ^ q) . 46 = q . 14 & (p ^ q) . 47 = q . 15 & (p ^ q) . 48 = q . 16 & (p ^ q) . 49 = q . 17 & (p ^ q) . 50 = q . 18 & (p ^ q) . 51 = q . 19 & (p ^ q) . 52 = q . 20 & (p ^ q) . 53 = q . 21 & (p ^ q) . 54 = q . 22 & (p ^ q) . 55 = q . 23 & (p ^ q) . 56 = q . 24 & (p ^ q) . 57 = q . 25 & (p ^ q) . 58 = q . 26 & (p ^ q) . 59 = q . 27 & (p ^ q) . 60 = q . 28 & (p ^ q) . 61 = q . 29 & (p ^ q) . 62 = q . 30 & (p ^ q) . 63 = q . 31 & (p ^ q) . 64 = q . 32 )
proof end;

theorem TT64: :: DESCIP_1:33
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 empty Nat;
let i be Element of n;
synonym ntoSeg i for succ n;
end;

definition
let n be non empty Nat;
let i be Element of 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 empty Nat;
let f be Function of n,(Seg n);
attr f is NtoSEG means :defNtoSEG: :: DESCIP_1:def 5
 for i being Element of n holds f . i = ntoSeg i;
end;

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

registration
let n be non empty Nat;
cluster V1() V4(n) V5( Seg n) Function-like non empty V21() total quasi_total V128() V129() V130() V131() NtoSEG for Element of bool [:n,(Seg n):];
existence
ex b1 being Function of n,(Seg n) st b1 is NtoSEG
proof end;
end;

RNGNtoSEG: for n being non empty Nat
for f being NtoSEG Function of n,(Seg n) holds rng f = Seg n
proof end;

registration
let n be non empty Nat;
cluster Function-like quasi_total NtoSEG -> bijective NtoSEG for Element of bool [:n,(Seg n):];
coherence
for b1 being NtoSEG Function of n,(Seg n) holds b1 is bijective
proof end;
end;

theorem ThL1: :: DESCIP_1:34
for n being non empty Nat
for f being NtoSEG Function of n,(Seg n)
for i being Nat st i < n holds
( f . i = i + 1 & i in dom f )
proof end;

ThL2: for f being NtoSEG Function of 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 ThL3: :: DESCIP_1:35
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;

LELEMNT16: ( 0 is Element of 16 & 1 is Element of 16 & 2 is Element of 16 & 3 is Element of 16 & 4 is Element of 16 & 5 is Element of 16 & 6 is Element of 16 & 7 is Element of 16 & 8 is Element of 16 & 9 is Element of 16 & 10 is Element of 16 & 11 is Element of 16 & 12 is Element of 16 & 13 is Element of 16 & 14 is Element of 16 & 15 is Element of 16 )
by NAT_1:44;

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

begin

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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ThL3, LELEMNT16;
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 LSBOXES;
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 ) );

begin

definition
let r be Element of 64 -tuples_on BOOLEAN;
func DES-IP r -> Element of 64 -tuples_on BOOLEAN means :defIP: :: 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 defIP 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 :defPIP: :: 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 defPIP 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 :defIPINV: :: 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 defIPINV 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 :defPIPINV: :: 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 defPIPINV 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 );

LTHIPP1: for x being Element of 64 -tuples_on BOOLEAN holds DES-IPINV (DES-IP x) = x
proof end;

LTHIPP2: for x being Element of 64 -tuples_on BOOLEAN holds DES-IP (DES-IPINV x) = x
proof end;

THIPP1: DES-PIPINV * DES-PIP = id (64 -tuples_on BOOLEAN)
proof end;

THIPP2: DES-PIP * DES-PIPINV = id (64 -tuples_on BOOLEAN)
proof end;

registration
cluster DES-PIP -> bijective ;
coherence
DES-PIP is bijective
proof end;
end;

registration
cluster DES-PIPINV -> bijective ;
correctness
coherence
DES-PIPINV is bijective ;
proof end;
end;

theorem :: DESCIP_1:36
DES-PIPINV = DES-PIP " by THIPP1, FUNCT_2:60;

begin

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 :DEFDIV8: :: 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 DEFDIV8 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 thDESDIV8: :: DESCIP_1:37
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;

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

ThL2L16: for f being NtoSEG Function of 16,(Seg 16)
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
for t being Element of 16 -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 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 )
proof end;

definition
func N16toB4 -> Function of 16,(4 -tuples_on BOOLEAN) means :: DESCIP_1:def 22
( it . 0 = <*0,0,0,0*> & it . 1 = <*0,0,0,1*> & it . 2 = <*0,0,1,0*> & it . 3 = <*0,0,1,1*> & it . 4 = <*0,1,0,0*> & it . 5 = <*0,1,0,1*> & it . 6 = <*0,1,1,0*> & it . 7 = <*0,1,1,1*> & it . 8 = <*1,0,0,0*> & it . 9 = <*1,0,0,1*> & it . 10 = <*1,0,1,0*> & it . 11 = <*1,0,1,1*> & it . 12 = <*1,1,0,0*> & it . 13 = <*1,1,0,1*> & it . 14 = <*1,1,1,0*> & it . 15 = <*1,1,1,1*> );
existence
ex b1 being Function of 16,(4 -tuples_on BOOLEAN) st
( b1 . 0 = <*0,0,0,0*> & b1 . 1 = <*0,0,0,1*> & b1 . 2 = <*0,0,1,0*> & b1 . 3 = <*0,0,1,1*> & b1 . 4 = <*0,1,0,0*> & b1 . 5 = <*0,1,0,1*> & b1 . 6 = <*0,1,1,0*> & b1 . 7 = <*0,1,1,1*> & b1 . 8 = <*1,0,0,0*> & b1 . 9 = <*1,0,0,1*> & b1 . 10 = <*1,0,1,0*> & b1 . 11 = <*1,0,1,1*> & b1 . 12 = <*1,1,0,0*> & b1 . 13 = <*1,1,0,1*> & b1 . 14 = <*1,1,1,0*> & b1 . 15 = <*1,1,1,1*> )
proof end;
uniqueness
for b1, b2 being Function of 16,(4 -tuples_on BOOLEAN) st b1 . 0 = <*0,0,0,0*> & b1 . 1 = <*0,0,0,1*> & b1 . 2 = <*0,0,1,0*> & b1 . 3 = <*0,0,1,1*> & b1 . 4 = <*0,1,0,0*> & b1 . 5 = <*0,1,0,1*> & b1 . 6 = <*0,1,1,0*> & b1 . 7 = <*0,1,1,1*> & b1 . 8 = <*1,0,0,0*> & b1 . 9 = <*1,0,0,1*> & b1 . 10 = <*1,0,1,0*> & b1 . 11 = <*1,0,1,1*> & b1 . 12 = <*1,1,0,0*> & b1 . 13 = <*1,1,0,1*> & b1 . 14 = <*1,1,1,0*> & b1 . 15 = <*1,1,1,1*> & b2 . 0 = <*0,0,0,0*> & b2 . 1 = <*0,0,0,1*> & b2 . 2 = <*0,0,1,0*> & b2 . 3 = <*0,0,1,1*> & b2 . 4 = <*0,1,0,0*> & b2 . 5 = <*0,1,0,1*> & b2 . 6 = <*0,1,1,0*> & b2 . 7 = <*0,1,1,1*> & b2 . 8 = <*1,0,0,0*> & b2 . 9 = <*1,0,0,1*> & b2 . 10 = <*1,0,1,0*> & b2 . 11 = <*1,0,1,1*> & b2 . 12 = <*1,1,0,0*> & b2 . 13 = <*1,1,0,1*> & b2 . 14 = <*1,1,1,0*> & b2 . 15 = <*1,1,1,1*> holds
b1 = b2
proof end;
end;

:: deftheorem defines N16toB4 DESCIP_1:def 22 :
for b1 being Function of 16,(4 -tuples_on BOOLEAN) holds
( b1 = N16toB4 iff ( b1 . 0 = <*0,0,0,0*> & b1 . 1 = <*0,0,0,1*> & b1 . 2 = <*0,0,1,0*> & b1 . 3 = <*0,0,1,1*> & b1 . 4 = <*0,1,0,0*> & b1 . 5 = <*0,1,0,1*> & b1 . 6 = <*0,1,1,0*> & b1 . 7 = <*0,1,1,1*> & b1 . 8 = <*1,0,0,0*> & b1 . 9 = <*1,0,0,1*> & b1 . 10 = <*1,0,1,0*> & b1 . 11 = <*1,0,1,1*> & b1 . 12 = <*1,1,0,0*> & b1 . 13 = <*1,1,0,1*> & b1 . 14 = <*1,1,1,0*> & b1 . 15 = <*1,1,1,1*> ) );

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

begin

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

begin

LM0102gen: for m, n, k being non empty 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 Element of 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 empty 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 :defOPDESlike: :: 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 Element of 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 Element of 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 LM0102gen;
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 Element of 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 Element of 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 defOPDESlike defines DES-like-CoDec DESCIP_1:def 29 :
for n, m, k being non empty 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 Element of 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 THMAINgen: :: DESCIP_1:38
for n, m, k being non empty 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 :defDESCODEC: :: 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 defDESCODEC 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 THMAIN: :: DESCIP_1:39
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:40
for message, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-DEC ((DES-ENC (message,secretkey)),secretkey) = message by THMAIN;