:: 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 proofend; 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 proofend; 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 proofend; :: original:Op-Right redefine func Op-Right (f,n) -> FinSequence of D; coherence Op-Right (f,n) is FinSequence of D proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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) ) ) proofend; 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 proofend; 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)) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; definition let x, y be Element of 28 -tuples_on BOOLEAN; :: original:^ redefine funcx ^ y -> Element of 56 -tuples_on BOOLEAN; coherence x ^ y is Element of 56 -tuples_on BOOLEAN proofend; 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 funcs . i -> Element of BOOLEAN ; coherence s . i is Element of BOOLEAN proofend; 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 funcs . i -> Element of NAT ; coherence s . i is Element of NAT proofend; 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 proofend; 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 proofend; 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) ) proofend; 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 funcRK . i -> Element of n -tuples_on BOOLEAN; coherence RK . i is Element of n -tuples_on BOOLEAN proofend; 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 proofend; 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 funcL . i -> Element of m -tuples_on D; coherence L . i is Element of m -tuples_on D proofend; end; definition let f be Function of 64,16; let i be set ; :: original:. redefine funcf . i -> Element of 16; coherence f . i is Element of 16 proofend; 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) proofend; 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] proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; theorem th1: :: DESCIP_1:24 for n being non empty Nat holds n = {0} \/ ((Seg n) \ {n}) proofend; 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 ) ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; end; definition let n be non empty Nat; let f be Function of n,(Seg n); attrf 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; clusterV1() 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 proofend; end; RNGNtoSEG: for n being non empty Nat for f being NtoSEG Function of n,(Seg n) holds rng f = Seg n proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; LTHIPP2: for x being Element of 64 -tuples_on BOOLEAN holds DES-IP (DES-IPINV x) = x proofend; THIPP1: DES-PIPINV * DES-PIP = id (64 -tuples_on BOOLEAN) proofend; THIPP2: DES-PIP * DES-PIPINV = id (64 -tuples_on BOOLEAN) proofend; registration cluster DES-PIP -> bijective ; coherence DES-PIP is bijective proofend; end; registration cluster DES-PIPINV -> bijective ; correctness coherence DES-PIPINV is bijective ; proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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) ) proofend; 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 proofend; 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 ) proofend; CTH1: for n being Nat for b being Element of BOOLEAN holds n * b <= n proofend; 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 proofend; 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 ) proofend; 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*> ) proofend; 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 proofend; 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 ) proofend; 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)) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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)) ) ) ) proofend; 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 proofend; 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)) ) proofend; 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 proofend; 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 proofend; 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) ) proofend; 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 proofend; 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;