scheme
QuadChoiceRec{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4()
-> non
empty set ,
F5()
-> Element of
F1(),
F6()
-> Element of
F2(),
F7()
-> Element of
F3(),
F8()
-> Element of
F4(),
P1[
object ,
object ,
object ,
object ,
object ,
object ,
object ,
object ,
object ] } :
provided
theorem Th21:
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 )
theorem Th22:
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 )
theorem Th23:
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 )
theorem Th24:
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 )
theorem Th25:
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 )
Lm1:
for n being non zero Nat
for f being NtoSEG Function of (Segm n),(Seg n) holds rng f = Seg n
Lm2:
for f being NtoSEG Function of (Segm 64),(Seg 64)
for S being non empty set
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of S
for t being Element of 64 -tuples_on S st t . 1 = x1 & t . 2 = x2 & t . 3 = x3 & t . 4 = x4 & t . 5 = x5 & t . 6 = x6 & t . 7 = x7 & t . 8 = x8 & t . 9 = x9 & t . 10 = x10 & t . 11 = x11 & t . 12 = x12 & t . 13 = x13 & t . 14 = x14 & t . 15 = x15 & t . 16 = x16 & t . 17 = x17 & t . 18 = x18 & t . 19 = x19 & t . 20 = x20 & t . 21 = x21 & t . 22 = x22 & t . 23 = x23 & t . 24 = x24 & t . 25 = x25 & t . 26 = x26 & t . 27 = x27 & t . 28 = x28 & t . 29 = x29 & t . 30 = x30 & t . 31 = x31 & t . 32 = x32 & t . 33 = x33 & t . 34 = x34 & t . 35 = x35 & t . 36 = x36 & t . 37 = x37 & t . 38 = x38 & t . 39 = x39 & t . 40 = x40 & t . 41 = x41 & t . 42 = x42 & t . 43 = x43 & t . 44 = x44 & t . 45 = x45 & t . 46 = x46 & t . 47 = x47 & t . 48 = x48 & t . 49 = x49 & t . 50 = x50 & t . 51 = x51 & t . 52 = x52 & t . 53 = x53 & t . 54 = x54 & t . 55 = x55 & t . 56 = x56 & t . 57 = x57 & t . 58 = x58 & t . 59 = x59 & t . 60 = x60 & t . 61 = x61 & t . 62 = x62 & t . 63 = x63 & t . 64 = x64 holds
( (t * f) . 0 = x1 & (t * f) . 1 = x2 & (t * f) . 2 = x3 & (t * f) . 3 = x4 & (t * f) . 4 = x5 & (t * f) . 5 = x6 & (t * f) . 6 = x7 & (t * f) . 7 = x8 & (t * f) . 8 = x9 & (t * f) . 9 = x10 & (t * f) . 10 = x11 & (t * f) . 11 = x12 & (t * f) . 12 = x13 & (t * f) . 13 = x14 & (t * f) . 14 = x15 & (t * f) . 15 = x16 & (t * f) . 16 = x17 & (t * f) . 17 = x18 & (t * f) . 18 = x19 & (t * f) . 19 = x20 & (t * f) . 20 = x21 & (t * f) . 21 = x22 & (t * f) . 22 = x23 & (t * f) . 23 = x24 & (t * f) . 24 = x25 & (t * f) . 25 = x26 & (t * f) . 26 = x27 & (t * f) . 27 = x28 & (t * f) . 28 = x29 & (t * f) . 29 = x30 & (t * f) . 30 = x31 & (t * f) . 31 = x32 & (t * f) . 32 = x33 & (t * f) . 33 = x34 & (t * f) . 34 = x35 & (t * f) . 35 = x36 & (t * f) . 36 = x37 & (t * f) . 37 = x38 & (t * f) . 38 = x39 & (t * f) . 39 = x40 & (t * f) . 40 = x41 & (t * f) . 41 = x42 & (t * f) . 42 = x43 & (t * f) . 43 = x44 & (t * f) . 44 = x45 & (t * f) . 45 = x46 & (t * f) . 46 = x47 & (t * f) . 47 = x48 & (t * f) . 48 = x49 & (t * f) . 49 = x50 & (t * f) . 50 = x51 & (t * f) . 51 = x52 & (t * f) . 52 = x53 & (t * f) . 53 = x54 & (t * f) . 54 = x55 & (t * f) . 55 = x56 & (t * f) . 56 = x57 & (t * f) . 57 = x58 & (t * f) . 58 = x59 & (t * f) . 59 = x60 & (t * f) . 60 = x61 & (t * f) . 61 = x62 & (t * f) . 62 = x63 & (t * f) . 63 = x64 )
theorem Th27:
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 )
Lm3:
0 is Element of Segm 16 & ... & 15 is Element of Segm 16
by NAT_1:44;
Lm4:
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64 being Element of 16
for f, g being Function of 64,16 st f . 1 = x1 & f . 2 = x2 & f . 3 = x3 & f . 4 = x4 & f . 5 = x5 & f . 6 = x6 & f . 7 = x7 & f . 8 = x8 & f . 9 = x9 & f . 10 = x10 & f . 11 = x11 & f . 12 = x12 & f . 13 = x13 & f . 14 = x14 & f . 15 = x15 & f . 16 = x16 & f . 17 = x17 & f . 18 = x18 & f . 19 = x19 & f . 20 = x20 & f . 21 = x21 & f . 22 = x22 & f . 23 = x23 & f . 24 = x24 & f . 25 = x25 & f . 26 = x26 & f . 27 = x27 & f . 28 = x28 & f . 29 = x29 & f . 30 = x30 & f . 31 = x31 & f . 32 = x32 & f . 33 = x33 & f . 34 = x34 & f . 35 = x35 & f . 36 = x36 & f . 37 = x37 & f . 38 = x38 & f . 39 = x39 & f . 40 = x40 & f . 41 = x41 & f . 42 = x42 & f . 43 = x43 & f . 44 = x44 & f . 45 = x45 & f . 46 = x46 & f . 47 = x47 & f . 48 = x48 & f . 49 = x49 & f . 50 = x50 & f . 51 = x51 & f . 52 = x52 & f . 53 = x53 & f . 54 = x54 & f . 55 = x55 & f . 56 = x56 & f . 57 = x57 & f . 58 = x58 & f . 59 = x59 & f . 60 = x60 & f . 61 = x61 & f . 62 = x62 & f . 63 = x63 & f . 0 = x64 & g . 1 = x1 & g . 2 = x2 & g . 3 = x3 & g . 4 = x4 & g . 5 = x5 & g . 6 = x6 & g . 7 = x7 & g . 8 = x8 & g . 9 = x9 & g . 10 = x10 & g . 11 = x11 & g . 12 = x12 & g . 13 = x13 & g . 14 = x14 & g . 15 = x15 & g . 16 = x16 & g . 17 = x17 & g . 18 = x18 & g . 19 = x19 & g . 20 = x20 & g . 21 = x21 & g . 22 = x22 & g . 23 = x23 & g . 24 = x24 & g . 25 = x25 & g . 26 = x26 & g . 27 = x27 & g . 28 = x28 & g . 29 = x29 & g . 30 = x30 & g . 31 = x31 & g . 32 = x32 & g . 33 = x33 & g . 34 = x34 & g . 35 = x35 & g . 36 = x36 & g . 37 = x37 & g . 38 = x38 & g . 39 = x39 & g . 40 = x40 & g . 41 = x41 & g . 42 = x42 & g . 43 = x43 & g . 44 = x44 & g . 45 = x45 & g . 46 = x46 & g . 47 = x47 & g . 48 = x48 & g . 49 = x49 & g . 50 = x50 & g . 51 = x51 & g . 52 = x52 & g . 53 = x53 & g . 54 = x54 & g . 55 = x55 & g . 56 = x56 & g . 57 = x57 & g . 58 = x58 & g . 59 = x59 & g . 60 = x60 & g . 61 = x61 & g . 62 = x62 & g . 63 = x63 & g . 0 = x64 holds
f = g
definition
func DES-SBOX1 -> Function of 64,16
means
(
it . 0 = 14 &
it . 1
= 4 &
it . 2
= 13 &
it . 3
= 1 &
it . 4
= 2 &
it . 5
= 15 &
it . 6
= 11 &
it . 7
= 8 &
it . 8
= 3 &
it . 9
= 10 &
it . 10
= 6 &
it . 11
= 12 &
it . 12
= 5 &
it . 13
= 9 &
it . 14
= 0 &
it . 15
= 7 &
it . 16
= 0 &
it . 17
= 15 &
it . 18
= 7 &
it . 19
= 4 &
it . 20
= 14 &
it . 21
= 2 &
it . 22
= 13 &
it . 23
= 1 &
it . 24
= 10 &
it . 25
= 6 &
it . 26
= 12 &
it . 27
= 11 &
it . 28
= 9 &
it . 29
= 5 &
it . 30
= 3 &
it . 31
= 8 &
it . 32
= 4 &
it . 33
= 1 &
it . 34
= 14 &
it . 35
= 8 &
it . 36
= 13 &
it . 37
= 6 &
it . 38
= 2 &
it . 39
= 11 &
it . 40
= 15 &
it . 41
= 12 &
it . 42
= 9 &
it . 43
= 7 &
it . 44
= 3 &
it . 45
= 10 &
it . 46
= 5 &
it . 47
= 0 &
it . 48
= 15 &
it . 49
= 12 &
it . 50
= 8 &
it . 51
= 2 &
it . 52
= 4 &
it . 53
= 9 &
it . 54
= 1 &
it . 55
= 7 &
it . 56
= 5 &
it . 57
= 11 &
it . 58
= 3 &
it . 59
= 14 &
it . 60
= 10 &
it . 61
= 0 &
it . 62
= 6 &
it . 63
= 13 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 14 & b1 . 1 = 4 & b1 . 2 = 13 & b1 . 3 = 1 & b1 . 4 = 2 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 8 & b1 . 8 = 3 & b1 . 9 = 10 & b1 . 10 = 6 & b1 . 11 = 12 & b1 . 12 = 5 & b1 . 13 = 9 & b1 . 14 = 0 & b1 . 15 = 7 & b1 . 16 = 0 & b1 . 17 = 15 & b1 . 18 = 7 & b1 . 19 = 4 & b1 . 20 = 14 & b1 . 21 = 2 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 10 & b1 . 25 = 6 & b1 . 26 = 12 & b1 . 27 = 11 & b1 . 28 = 9 & b1 . 29 = 5 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 4 & b1 . 33 = 1 & b1 . 34 = 14 & b1 . 35 = 8 & b1 . 36 = 13 & b1 . 37 = 6 & b1 . 38 = 2 & b1 . 39 = 11 & b1 . 40 = 15 & b1 . 41 = 12 & b1 . 42 = 9 & b1 . 43 = 7 & b1 . 44 = 3 & b1 . 45 = 10 & b1 . 46 = 5 & b1 . 47 = 0 & b1 . 48 = 15 & b1 . 49 = 12 & b1 . 50 = 8 & b1 . 51 = 2 & b1 . 52 = 4 & b1 . 53 = 9 & b1 . 54 = 1 & b1 . 55 = 7 & b1 . 56 = 5 & b1 . 57 = 11 & b1 . 58 = 3 & b1 . 59 = 14 & b1 . 60 = 10 & b1 . 61 = 0 & b1 . 62 = 6 & b1 . 63 = 13 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 14 & b1 . 1 = 4 & b1 . 2 = 13 & b1 . 3 = 1 & b1 . 4 = 2 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 8 & b1 . 8 = 3 & b1 . 9 = 10 & b1 . 10 = 6 & b1 . 11 = 12 & b1 . 12 = 5 & b1 . 13 = 9 & b1 . 14 = 0 & b1 . 15 = 7 & b1 . 16 = 0 & b1 . 17 = 15 & b1 . 18 = 7 & b1 . 19 = 4 & b1 . 20 = 14 & b1 . 21 = 2 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 10 & b1 . 25 = 6 & b1 . 26 = 12 & b1 . 27 = 11 & b1 . 28 = 9 & b1 . 29 = 5 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 4 & b1 . 33 = 1 & b1 . 34 = 14 & b1 . 35 = 8 & b1 . 36 = 13 & b1 . 37 = 6 & b1 . 38 = 2 & b1 . 39 = 11 & b1 . 40 = 15 & b1 . 41 = 12 & b1 . 42 = 9 & b1 . 43 = 7 & b1 . 44 = 3 & b1 . 45 = 10 & b1 . 46 = 5 & b1 . 47 = 0 & b1 . 48 = 15 & b1 . 49 = 12 & b1 . 50 = 8 & b1 . 51 = 2 & b1 . 52 = 4 & b1 . 53 = 9 & b1 . 54 = 1 & b1 . 55 = 7 & b1 . 56 = 5 & b1 . 57 = 11 & b1 . 58 = 3 & b1 . 59 = 14 & b1 . 60 = 10 & b1 . 61 = 0 & b1 . 62 = 6 & b1 . 63 = 13 & b2 . 0 = 14 & b2 . 1 = 4 & b2 . 2 = 13 & b2 . 3 = 1 & b2 . 4 = 2 & b2 . 5 = 15 & b2 . 6 = 11 & b2 . 7 = 8 & b2 . 8 = 3 & b2 . 9 = 10 & b2 . 10 = 6 & b2 . 11 = 12 & b2 . 12 = 5 & b2 . 13 = 9 & b2 . 14 = 0 & b2 . 15 = 7 & b2 . 16 = 0 & b2 . 17 = 15 & b2 . 18 = 7 & b2 . 19 = 4 & b2 . 20 = 14 & b2 . 21 = 2 & b2 . 22 = 13 & b2 . 23 = 1 & b2 . 24 = 10 & b2 . 25 = 6 & b2 . 26 = 12 & b2 . 27 = 11 & b2 . 28 = 9 & b2 . 29 = 5 & b2 . 30 = 3 & b2 . 31 = 8 & b2 . 32 = 4 & b2 . 33 = 1 & b2 . 34 = 14 & b2 . 35 = 8 & b2 . 36 = 13 & b2 . 37 = 6 & b2 . 38 = 2 & b2 . 39 = 11 & b2 . 40 = 15 & b2 . 41 = 12 & b2 . 42 = 9 & b2 . 43 = 7 & b2 . 44 = 3 & b2 . 45 = 10 & b2 . 46 = 5 & b2 . 47 = 0 & b2 . 48 = 15 & b2 . 49 = 12 & b2 . 50 = 8 & b2 . 51 = 2 & b2 . 52 = 4 & b2 . 53 = 9 & b2 . 54 = 1 & b2 . 55 = 7 & b2 . 56 = 5 & b2 . 57 = 11 & b2 . 58 = 3 & b2 . 59 = 14 & b2 . 60 = 10 & b2 . 61 = 0 & b2 . 62 = 6 & b2 . 63 = 13 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX1 DESCIP_1:def 6 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX1 iff ( b1 . 0 = 14 & b1 . 1 = 4 & b1 . 2 = 13 & b1 . 3 = 1 & b1 . 4 = 2 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 8 & b1 . 8 = 3 & b1 . 9 = 10 & b1 . 10 = 6 & b1 . 11 = 12 & b1 . 12 = 5 & b1 . 13 = 9 & b1 . 14 = 0 & b1 . 15 = 7 & b1 . 16 = 0 & b1 . 17 = 15 & b1 . 18 = 7 & b1 . 19 = 4 & b1 . 20 = 14 & b1 . 21 = 2 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 10 & b1 . 25 = 6 & b1 . 26 = 12 & b1 . 27 = 11 & b1 . 28 = 9 & b1 . 29 = 5 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 4 & b1 . 33 = 1 & b1 . 34 = 14 & b1 . 35 = 8 & b1 . 36 = 13 & b1 . 37 = 6 & b1 . 38 = 2 & b1 . 39 = 11 & b1 . 40 = 15 & b1 . 41 = 12 & b1 . 42 = 9 & b1 . 43 = 7 & b1 . 44 = 3 & b1 . 45 = 10 & b1 . 46 = 5 & b1 . 47 = 0 & b1 . 48 = 15 & b1 . 49 = 12 & b1 . 50 = 8 & b1 . 51 = 2 & b1 . 52 = 4 & b1 . 53 = 9 & b1 . 54 = 1 & b1 . 55 = 7 & b1 . 56 = 5 & b1 . 57 = 11 & b1 . 58 = 3 & b1 . 59 = 14 & b1 . 60 = 10 & b1 . 61 = 0 & b1 . 62 = 6 & b1 . 63 = 13 ) );
definition
func DES-SBOX2 -> Function of 64,16
means
(
it . 0 = 15 &
it . 1
= 1 &
it . 2
= 8 &
it . 3
= 14 &
it . 4
= 6 &
it . 5
= 11 &
it . 6
= 3 &
it . 7
= 4 &
it . 8
= 9 &
it . 9
= 7 &
it . 10
= 2 &
it . 11
= 13 &
it . 12
= 12 &
it . 13
= 0 &
it . 14
= 5 &
it . 15
= 10 &
it . 16
= 3 &
it . 17
= 13 &
it . 18
= 4 &
it . 19
= 7 &
it . 20
= 15 &
it . 21
= 2 &
it . 22
= 8 &
it . 23
= 14 &
it . 24
= 12 &
it . 25
= 0 &
it . 26
= 1 &
it . 27
= 10 &
it . 28
= 6 &
it . 29
= 9 &
it . 30
= 11 &
it . 31
= 5 &
it . 32
= 0 &
it . 33
= 14 &
it . 34
= 7 &
it . 35
= 11 &
it . 36
= 10 &
it . 37
= 4 &
it . 38
= 13 &
it . 39
= 1 &
it . 40
= 5 &
it . 41
= 8 &
it . 42
= 12 &
it . 43
= 6 &
it . 44
= 9 &
it . 45
= 3 &
it . 46
= 2 &
it . 47
= 15 &
it . 48
= 13 &
it . 49
= 8 &
it . 50
= 10 &
it . 51
= 1 &
it . 52
= 3 &
it . 53
= 15 &
it . 54
= 4 &
it . 55
= 2 &
it . 56
= 11 &
it . 57
= 6 &
it . 58
= 7 &
it . 59
= 12 &
it . 60
= 0 &
it . 61
= 5 &
it . 62
= 14 &
it . 63
= 9 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 15 & b1 . 1 = 1 & b1 . 2 = 8 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 11 & b1 . 6 = 3 & b1 . 7 = 4 & b1 . 8 = 9 & b1 . 9 = 7 & b1 . 10 = 2 & b1 . 11 = 13 & b1 . 12 = 12 & b1 . 13 = 0 & b1 . 14 = 5 & b1 . 15 = 10 & b1 . 16 = 3 & b1 . 17 = 13 & b1 . 18 = 4 & b1 . 19 = 7 & b1 . 20 = 15 & b1 . 21 = 2 & b1 . 22 = 8 & b1 . 23 = 14 & b1 . 24 = 12 & b1 . 25 = 0 & b1 . 26 = 1 & b1 . 27 = 10 & b1 . 28 = 6 & b1 . 29 = 9 & b1 . 30 = 11 & b1 . 31 = 5 & b1 . 32 = 0 & b1 . 33 = 14 & b1 . 34 = 7 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 4 & b1 . 38 = 13 & b1 . 39 = 1 & b1 . 40 = 5 & b1 . 41 = 8 & b1 . 42 = 12 & b1 . 43 = 6 & b1 . 44 = 9 & b1 . 45 = 3 & b1 . 46 = 2 & b1 . 47 = 15 & b1 . 48 = 13 & b1 . 49 = 8 & b1 . 50 = 10 & b1 . 51 = 1 & b1 . 52 = 3 & b1 . 53 = 15 & b1 . 54 = 4 & b1 . 55 = 2 & b1 . 56 = 11 & b1 . 57 = 6 & b1 . 58 = 7 & b1 . 59 = 12 & b1 . 60 = 0 & b1 . 61 = 5 & b1 . 62 = 14 & b1 . 63 = 9 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 15 & b1 . 1 = 1 & b1 . 2 = 8 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 11 & b1 . 6 = 3 & b1 . 7 = 4 & b1 . 8 = 9 & b1 . 9 = 7 & b1 . 10 = 2 & b1 . 11 = 13 & b1 . 12 = 12 & b1 . 13 = 0 & b1 . 14 = 5 & b1 . 15 = 10 & b1 . 16 = 3 & b1 . 17 = 13 & b1 . 18 = 4 & b1 . 19 = 7 & b1 . 20 = 15 & b1 . 21 = 2 & b1 . 22 = 8 & b1 . 23 = 14 & b1 . 24 = 12 & b1 . 25 = 0 & b1 . 26 = 1 & b1 . 27 = 10 & b1 . 28 = 6 & b1 . 29 = 9 & b1 . 30 = 11 & b1 . 31 = 5 & b1 . 32 = 0 & b1 . 33 = 14 & b1 . 34 = 7 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 4 & b1 . 38 = 13 & b1 . 39 = 1 & b1 . 40 = 5 & b1 . 41 = 8 & b1 . 42 = 12 & b1 . 43 = 6 & b1 . 44 = 9 & b1 . 45 = 3 & b1 . 46 = 2 & b1 . 47 = 15 & b1 . 48 = 13 & b1 . 49 = 8 & b1 . 50 = 10 & b1 . 51 = 1 & b1 . 52 = 3 & b1 . 53 = 15 & b1 . 54 = 4 & b1 . 55 = 2 & b1 . 56 = 11 & b1 . 57 = 6 & b1 . 58 = 7 & b1 . 59 = 12 & b1 . 60 = 0 & b1 . 61 = 5 & b1 . 62 = 14 & b1 . 63 = 9 & b2 . 0 = 15 & b2 . 1 = 1 & b2 . 2 = 8 & b2 . 3 = 14 & b2 . 4 = 6 & b2 . 5 = 11 & b2 . 6 = 3 & b2 . 7 = 4 & b2 . 8 = 9 & b2 . 9 = 7 & b2 . 10 = 2 & b2 . 11 = 13 & b2 . 12 = 12 & b2 . 13 = 0 & b2 . 14 = 5 & b2 . 15 = 10 & b2 . 16 = 3 & b2 . 17 = 13 & b2 . 18 = 4 & b2 . 19 = 7 & b2 . 20 = 15 & b2 . 21 = 2 & b2 . 22 = 8 & b2 . 23 = 14 & b2 . 24 = 12 & b2 . 25 = 0 & b2 . 26 = 1 & b2 . 27 = 10 & b2 . 28 = 6 & b2 . 29 = 9 & b2 . 30 = 11 & b2 . 31 = 5 & b2 . 32 = 0 & b2 . 33 = 14 & b2 . 34 = 7 & b2 . 35 = 11 & b2 . 36 = 10 & b2 . 37 = 4 & b2 . 38 = 13 & b2 . 39 = 1 & b2 . 40 = 5 & b2 . 41 = 8 & b2 . 42 = 12 & b2 . 43 = 6 & b2 . 44 = 9 & b2 . 45 = 3 & b2 . 46 = 2 & b2 . 47 = 15 & b2 . 48 = 13 & b2 . 49 = 8 & b2 . 50 = 10 & b2 . 51 = 1 & b2 . 52 = 3 & b2 . 53 = 15 & b2 . 54 = 4 & b2 . 55 = 2 & b2 . 56 = 11 & b2 . 57 = 6 & b2 . 58 = 7 & b2 . 59 = 12 & b2 . 60 = 0 & b2 . 61 = 5 & b2 . 62 = 14 & b2 . 63 = 9 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX2 DESCIP_1:def 7 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX2 iff ( b1 . 0 = 15 & b1 . 1 = 1 & b1 . 2 = 8 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 11 & b1 . 6 = 3 & b1 . 7 = 4 & b1 . 8 = 9 & b1 . 9 = 7 & b1 . 10 = 2 & b1 . 11 = 13 & b1 . 12 = 12 & b1 . 13 = 0 & b1 . 14 = 5 & b1 . 15 = 10 & b1 . 16 = 3 & b1 . 17 = 13 & b1 . 18 = 4 & b1 . 19 = 7 & b1 . 20 = 15 & b1 . 21 = 2 & b1 . 22 = 8 & b1 . 23 = 14 & b1 . 24 = 12 & b1 . 25 = 0 & b1 . 26 = 1 & b1 . 27 = 10 & b1 . 28 = 6 & b1 . 29 = 9 & b1 . 30 = 11 & b1 . 31 = 5 & b1 . 32 = 0 & b1 . 33 = 14 & b1 . 34 = 7 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 4 & b1 . 38 = 13 & b1 . 39 = 1 & b1 . 40 = 5 & b1 . 41 = 8 & b1 . 42 = 12 & b1 . 43 = 6 & b1 . 44 = 9 & b1 . 45 = 3 & b1 . 46 = 2 & b1 . 47 = 15 & b1 . 48 = 13 & b1 . 49 = 8 & b1 . 50 = 10 & b1 . 51 = 1 & b1 . 52 = 3 & b1 . 53 = 15 & b1 . 54 = 4 & b1 . 55 = 2 & b1 . 56 = 11 & b1 . 57 = 6 & b1 . 58 = 7 & b1 . 59 = 12 & b1 . 60 = 0 & b1 . 61 = 5 & b1 . 62 = 14 & b1 . 63 = 9 ) );
definition
func DES-SBOX3 -> Function of 64,16
means
(
it . 0 = 10 &
it . 1
= 0 &
it . 2
= 9 &
it . 3
= 14 &
it . 4
= 6 &
it . 5
= 3 &
it . 6
= 15 &
it . 7
= 5 &
it . 8
= 1 &
it . 9
= 13 &
it . 10
= 12 &
it . 11
= 7 &
it . 12
= 11 &
it . 13
= 4 &
it . 14
= 2 &
it . 15
= 8 &
it . 16
= 13 &
it . 17
= 7 &
it . 18
= 0 &
it . 19
= 9 &
it . 20
= 3 &
it . 21
= 4 &
it . 22
= 6 &
it . 23
= 10 &
it . 24
= 2 &
it . 25
= 8 &
it . 26
= 5 &
it . 27
= 14 &
it . 28
= 12 &
it . 29
= 11 &
it . 30
= 15 &
it . 31
= 1 &
it . 32
= 13 &
it . 33
= 6 &
it . 34
= 4 &
it . 35
= 9 &
it . 36
= 8 &
it . 37
= 15 &
it . 38
= 3 &
it . 39
= 0 &
it . 40
= 11 &
it . 41
= 1 &
it . 42
= 2 &
it . 43
= 12 &
it . 44
= 5 &
it . 45
= 10 &
it . 46
= 14 &
it . 47
= 7 &
it . 48
= 1 &
it . 49
= 10 &
it . 50
= 13 &
it . 51
= 0 &
it . 52
= 6 &
it . 53
= 9 &
it . 54
= 8 &
it . 55
= 7 &
it . 56
= 4 &
it . 57
= 15 &
it . 58
= 14 &
it . 59
= 3 &
it . 60
= 11 &
it . 61
= 5 &
it . 62
= 2 &
it . 63
= 12 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 10 & b1 . 1 = 0 & b1 . 2 = 9 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 3 & b1 . 6 = 15 & b1 . 7 = 5 & b1 . 8 = 1 & b1 . 9 = 13 & b1 . 10 = 12 & b1 . 11 = 7 & b1 . 12 = 11 & b1 . 13 = 4 & b1 . 14 = 2 & b1 . 15 = 8 & b1 . 16 = 13 & b1 . 17 = 7 & b1 . 18 = 0 & b1 . 19 = 9 & b1 . 20 = 3 & b1 . 21 = 4 & b1 . 22 = 6 & b1 . 23 = 10 & b1 . 24 = 2 & b1 . 25 = 8 & b1 . 26 = 5 & b1 . 27 = 14 & b1 . 28 = 12 & b1 . 29 = 11 & b1 . 30 = 15 & b1 . 31 = 1 & b1 . 32 = 13 & b1 . 33 = 6 & b1 . 34 = 4 & b1 . 35 = 9 & b1 . 36 = 8 & b1 . 37 = 15 & b1 . 38 = 3 & b1 . 39 = 0 & b1 . 40 = 11 & b1 . 41 = 1 & b1 . 42 = 2 & b1 . 43 = 12 & b1 . 44 = 5 & b1 . 45 = 10 & b1 . 46 = 14 & b1 . 47 = 7 & b1 . 48 = 1 & b1 . 49 = 10 & b1 . 50 = 13 & b1 . 51 = 0 & b1 . 52 = 6 & b1 . 53 = 9 & b1 . 54 = 8 & b1 . 55 = 7 & b1 . 56 = 4 & b1 . 57 = 15 & b1 . 58 = 14 & b1 . 59 = 3 & b1 . 60 = 11 & b1 . 61 = 5 & b1 . 62 = 2 & b1 . 63 = 12 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 10 & b1 . 1 = 0 & b1 . 2 = 9 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 3 & b1 . 6 = 15 & b1 . 7 = 5 & b1 . 8 = 1 & b1 . 9 = 13 & b1 . 10 = 12 & b1 . 11 = 7 & b1 . 12 = 11 & b1 . 13 = 4 & b1 . 14 = 2 & b1 . 15 = 8 & b1 . 16 = 13 & b1 . 17 = 7 & b1 . 18 = 0 & b1 . 19 = 9 & b1 . 20 = 3 & b1 . 21 = 4 & b1 . 22 = 6 & b1 . 23 = 10 & b1 . 24 = 2 & b1 . 25 = 8 & b1 . 26 = 5 & b1 . 27 = 14 & b1 . 28 = 12 & b1 . 29 = 11 & b1 . 30 = 15 & b1 . 31 = 1 & b1 . 32 = 13 & b1 . 33 = 6 & b1 . 34 = 4 & b1 . 35 = 9 & b1 . 36 = 8 & b1 . 37 = 15 & b1 . 38 = 3 & b1 . 39 = 0 & b1 . 40 = 11 & b1 . 41 = 1 & b1 . 42 = 2 & b1 . 43 = 12 & b1 . 44 = 5 & b1 . 45 = 10 & b1 . 46 = 14 & b1 . 47 = 7 & b1 . 48 = 1 & b1 . 49 = 10 & b1 . 50 = 13 & b1 . 51 = 0 & b1 . 52 = 6 & b1 . 53 = 9 & b1 . 54 = 8 & b1 . 55 = 7 & b1 . 56 = 4 & b1 . 57 = 15 & b1 . 58 = 14 & b1 . 59 = 3 & b1 . 60 = 11 & b1 . 61 = 5 & b1 . 62 = 2 & b1 . 63 = 12 & b2 . 0 = 10 & b2 . 1 = 0 & b2 . 2 = 9 & b2 . 3 = 14 & b2 . 4 = 6 & b2 . 5 = 3 & b2 . 6 = 15 & b2 . 7 = 5 & b2 . 8 = 1 & b2 . 9 = 13 & b2 . 10 = 12 & b2 . 11 = 7 & b2 . 12 = 11 & b2 . 13 = 4 & b2 . 14 = 2 & b2 . 15 = 8 & b2 . 16 = 13 & b2 . 17 = 7 & b2 . 18 = 0 & b2 . 19 = 9 & b2 . 20 = 3 & b2 . 21 = 4 & b2 . 22 = 6 & b2 . 23 = 10 & b2 . 24 = 2 & b2 . 25 = 8 & b2 . 26 = 5 & b2 . 27 = 14 & b2 . 28 = 12 & b2 . 29 = 11 & b2 . 30 = 15 & b2 . 31 = 1 & b2 . 32 = 13 & b2 . 33 = 6 & b2 . 34 = 4 & b2 . 35 = 9 & b2 . 36 = 8 & b2 . 37 = 15 & b2 . 38 = 3 & b2 . 39 = 0 & b2 . 40 = 11 & b2 . 41 = 1 & b2 . 42 = 2 & b2 . 43 = 12 & b2 . 44 = 5 & b2 . 45 = 10 & b2 . 46 = 14 & b2 . 47 = 7 & b2 . 48 = 1 & b2 . 49 = 10 & b2 . 50 = 13 & b2 . 51 = 0 & b2 . 52 = 6 & b2 . 53 = 9 & b2 . 54 = 8 & b2 . 55 = 7 & b2 . 56 = 4 & b2 . 57 = 15 & b2 . 58 = 14 & b2 . 59 = 3 & b2 . 60 = 11 & b2 . 61 = 5 & b2 . 62 = 2 & b2 . 63 = 12 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX3 DESCIP_1:def 8 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX3 iff ( b1 . 0 = 10 & b1 . 1 = 0 & b1 . 2 = 9 & b1 . 3 = 14 & b1 . 4 = 6 & b1 . 5 = 3 & b1 . 6 = 15 & b1 . 7 = 5 & b1 . 8 = 1 & b1 . 9 = 13 & b1 . 10 = 12 & b1 . 11 = 7 & b1 . 12 = 11 & b1 . 13 = 4 & b1 . 14 = 2 & b1 . 15 = 8 & b1 . 16 = 13 & b1 . 17 = 7 & b1 . 18 = 0 & b1 . 19 = 9 & b1 . 20 = 3 & b1 . 21 = 4 & b1 . 22 = 6 & b1 . 23 = 10 & b1 . 24 = 2 & b1 . 25 = 8 & b1 . 26 = 5 & b1 . 27 = 14 & b1 . 28 = 12 & b1 . 29 = 11 & b1 . 30 = 15 & b1 . 31 = 1 & b1 . 32 = 13 & b1 . 33 = 6 & b1 . 34 = 4 & b1 . 35 = 9 & b1 . 36 = 8 & b1 . 37 = 15 & b1 . 38 = 3 & b1 . 39 = 0 & b1 . 40 = 11 & b1 . 41 = 1 & b1 . 42 = 2 & b1 . 43 = 12 & b1 . 44 = 5 & b1 . 45 = 10 & b1 . 46 = 14 & b1 . 47 = 7 & b1 . 48 = 1 & b1 . 49 = 10 & b1 . 50 = 13 & b1 . 51 = 0 & b1 . 52 = 6 & b1 . 53 = 9 & b1 . 54 = 8 & b1 . 55 = 7 & b1 . 56 = 4 & b1 . 57 = 15 & b1 . 58 = 14 & b1 . 59 = 3 & b1 . 60 = 11 & b1 . 61 = 5 & b1 . 62 = 2 & b1 . 63 = 12 ) );
definition
func DES-SBOX4 -> Function of 64,16
means
(
it . 0 = 7 &
it . 1
= 13 &
it . 2
= 14 &
it . 3
= 3 &
it . 4
= 0 &
it . 5
= 6 &
it . 6
= 9 &
it . 7
= 10 &
it . 8
= 1 &
it . 9
= 2 &
it . 10
= 8 &
it . 11
= 5 &
it . 12
= 11 &
it . 13
= 12 &
it . 14
= 4 &
it . 15
= 15 &
it . 16
= 13 &
it . 17
= 8 &
it . 18
= 11 &
it . 19
= 5 &
it . 20
= 6 &
it . 21
= 15 &
it . 22
= 0 &
it . 23
= 3 &
it . 24
= 4 &
it . 25
= 7 &
it . 26
= 2 &
it . 27
= 12 &
it . 28
= 1 &
it . 29
= 10 &
it . 30
= 14 &
it . 31
= 9 &
it . 32
= 10 &
it . 33
= 6 &
it . 34
= 9 &
it . 35
= 0 &
it . 36
= 12 &
it . 37
= 11 &
it . 38
= 7 &
it . 39
= 13 &
it . 40
= 15 &
it . 41
= 1 &
it . 42
= 3 &
it . 43
= 14 &
it . 44
= 5 &
it . 45
= 2 &
it . 46
= 8 &
it . 47
= 4 &
it . 48
= 3 &
it . 49
= 15 &
it . 50
= 0 &
it . 51
= 6 &
it . 52
= 10 &
it . 53
= 1 &
it . 54
= 13 &
it . 55
= 8 &
it . 56
= 9 &
it . 57
= 4 &
it . 58
= 5 &
it . 59
= 11 &
it . 60
= 12 &
it . 61
= 7 &
it . 62
= 2 &
it . 63
= 14 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 7 & b1 . 1 = 13 & b1 . 2 = 14 & b1 . 3 = 3 & b1 . 4 = 0 & b1 . 5 = 6 & b1 . 6 = 9 & b1 . 7 = 10 & b1 . 8 = 1 & b1 . 9 = 2 & b1 . 10 = 8 & b1 . 11 = 5 & b1 . 12 = 11 & b1 . 13 = 12 & b1 . 14 = 4 & b1 . 15 = 15 & b1 . 16 = 13 & b1 . 17 = 8 & b1 . 18 = 11 & b1 . 19 = 5 & b1 . 20 = 6 & b1 . 21 = 15 & b1 . 22 = 0 & b1 . 23 = 3 & b1 . 24 = 4 & b1 . 25 = 7 & b1 . 26 = 2 & b1 . 27 = 12 & b1 . 28 = 1 & b1 . 29 = 10 & b1 . 30 = 14 & b1 . 31 = 9 & b1 . 32 = 10 & b1 . 33 = 6 & b1 . 34 = 9 & b1 . 35 = 0 & b1 . 36 = 12 & b1 . 37 = 11 & b1 . 38 = 7 & b1 . 39 = 13 & b1 . 40 = 15 & b1 . 41 = 1 & b1 . 42 = 3 & b1 . 43 = 14 & b1 . 44 = 5 & b1 . 45 = 2 & b1 . 46 = 8 & b1 . 47 = 4 & b1 . 48 = 3 & b1 . 49 = 15 & b1 . 50 = 0 & b1 . 51 = 6 & b1 . 52 = 10 & b1 . 53 = 1 & b1 . 54 = 13 & b1 . 55 = 8 & b1 . 56 = 9 & b1 . 57 = 4 & b1 . 58 = 5 & b1 . 59 = 11 & b1 . 60 = 12 & b1 . 61 = 7 & b1 . 62 = 2 & b1 . 63 = 14 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 7 & b1 . 1 = 13 & b1 . 2 = 14 & b1 . 3 = 3 & b1 . 4 = 0 & b1 . 5 = 6 & b1 . 6 = 9 & b1 . 7 = 10 & b1 . 8 = 1 & b1 . 9 = 2 & b1 . 10 = 8 & b1 . 11 = 5 & b1 . 12 = 11 & b1 . 13 = 12 & b1 . 14 = 4 & b1 . 15 = 15 & b1 . 16 = 13 & b1 . 17 = 8 & b1 . 18 = 11 & b1 . 19 = 5 & b1 . 20 = 6 & b1 . 21 = 15 & b1 . 22 = 0 & b1 . 23 = 3 & b1 . 24 = 4 & b1 . 25 = 7 & b1 . 26 = 2 & b1 . 27 = 12 & b1 . 28 = 1 & b1 . 29 = 10 & b1 . 30 = 14 & b1 . 31 = 9 & b1 . 32 = 10 & b1 . 33 = 6 & b1 . 34 = 9 & b1 . 35 = 0 & b1 . 36 = 12 & b1 . 37 = 11 & b1 . 38 = 7 & b1 . 39 = 13 & b1 . 40 = 15 & b1 . 41 = 1 & b1 . 42 = 3 & b1 . 43 = 14 & b1 . 44 = 5 & b1 . 45 = 2 & b1 . 46 = 8 & b1 . 47 = 4 & b1 . 48 = 3 & b1 . 49 = 15 & b1 . 50 = 0 & b1 . 51 = 6 & b1 . 52 = 10 & b1 . 53 = 1 & b1 . 54 = 13 & b1 . 55 = 8 & b1 . 56 = 9 & b1 . 57 = 4 & b1 . 58 = 5 & b1 . 59 = 11 & b1 . 60 = 12 & b1 . 61 = 7 & b1 . 62 = 2 & b1 . 63 = 14 & b2 . 0 = 7 & b2 . 1 = 13 & b2 . 2 = 14 & b2 . 3 = 3 & b2 . 4 = 0 & b2 . 5 = 6 & b2 . 6 = 9 & b2 . 7 = 10 & b2 . 8 = 1 & b2 . 9 = 2 & b2 . 10 = 8 & b2 . 11 = 5 & b2 . 12 = 11 & b2 . 13 = 12 & b2 . 14 = 4 & b2 . 15 = 15 & b2 . 16 = 13 & b2 . 17 = 8 & b2 . 18 = 11 & b2 . 19 = 5 & b2 . 20 = 6 & b2 . 21 = 15 & b2 . 22 = 0 & b2 . 23 = 3 & b2 . 24 = 4 & b2 . 25 = 7 & b2 . 26 = 2 & b2 . 27 = 12 & b2 . 28 = 1 & b2 . 29 = 10 & b2 . 30 = 14 & b2 . 31 = 9 & b2 . 32 = 10 & b2 . 33 = 6 & b2 . 34 = 9 & b2 . 35 = 0 & b2 . 36 = 12 & b2 . 37 = 11 & b2 . 38 = 7 & b2 . 39 = 13 & b2 . 40 = 15 & b2 . 41 = 1 & b2 . 42 = 3 & b2 . 43 = 14 & b2 . 44 = 5 & b2 . 45 = 2 & b2 . 46 = 8 & b2 . 47 = 4 & b2 . 48 = 3 & b2 . 49 = 15 & b2 . 50 = 0 & b2 . 51 = 6 & b2 . 52 = 10 & b2 . 53 = 1 & b2 . 54 = 13 & b2 . 55 = 8 & b2 . 56 = 9 & b2 . 57 = 4 & b2 . 58 = 5 & b2 . 59 = 11 & b2 . 60 = 12 & b2 . 61 = 7 & b2 . 62 = 2 & b2 . 63 = 14 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX4 DESCIP_1:def 9 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX4 iff ( b1 . 0 = 7 & b1 . 1 = 13 & b1 . 2 = 14 & b1 . 3 = 3 & b1 . 4 = 0 & b1 . 5 = 6 & b1 . 6 = 9 & b1 . 7 = 10 & b1 . 8 = 1 & b1 . 9 = 2 & b1 . 10 = 8 & b1 . 11 = 5 & b1 . 12 = 11 & b1 . 13 = 12 & b1 . 14 = 4 & b1 . 15 = 15 & b1 . 16 = 13 & b1 . 17 = 8 & b1 . 18 = 11 & b1 . 19 = 5 & b1 . 20 = 6 & b1 . 21 = 15 & b1 . 22 = 0 & b1 . 23 = 3 & b1 . 24 = 4 & b1 . 25 = 7 & b1 . 26 = 2 & b1 . 27 = 12 & b1 . 28 = 1 & b1 . 29 = 10 & b1 . 30 = 14 & b1 . 31 = 9 & b1 . 32 = 10 & b1 . 33 = 6 & b1 . 34 = 9 & b1 . 35 = 0 & b1 . 36 = 12 & b1 . 37 = 11 & b1 . 38 = 7 & b1 . 39 = 13 & b1 . 40 = 15 & b1 . 41 = 1 & b1 . 42 = 3 & b1 . 43 = 14 & b1 . 44 = 5 & b1 . 45 = 2 & b1 . 46 = 8 & b1 . 47 = 4 & b1 . 48 = 3 & b1 . 49 = 15 & b1 . 50 = 0 & b1 . 51 = 6 & b1 . 52 = 10 & b1 . 53 = 1 & b1 . 54 = 13 & b1 . 55 = 8 & b1 . 56 = 9 & b1 . 57 = 4 & b1 . 58 = 5 & b1 . 59 = 11 & b1 . 60 = 12 & b1 . 61 = 7 & b1 . 62 = 2 & b1 . 63 = 14 ) );
definition
func DES-SBOX5 -> Function of 64,16
means
(
it . 0 = 2 &
it . 1
= 12 &
it . 2
= 4 &
it . 3
= 1 &
it . 4
= 7 &
it . 5
= 10 &
it . 6
= 11 &
it . 7
= 6 &
it . 8
= 8 &
it . 9
= 5 &
it . 10
= 3 &
it . 11
= 15 &
it . 12
= 13 &
it . 13
= 0 &
it . 14
= 14 &
it . 15
= 9 &
it . 16
= 14 &
it . 17
= 11 &
it . 18
= 2 &
it . 19
= 12 &
it . 20
= 4 &
it . 21
= 7 &
it . 22
= 13 &
it . 23
= 1 &
it . 24
= 5 &
it . 25
= 0 &
it . 26
= 15 &
it . 27
= 10 &
it . 28
= 3 &
it . 29
= 9 &
it . 30
= 8 &
it . 31
= 6 &
it . 32
= 4 &
it . 33
= 2 &
it . 34
= 1 &
it . 35
= 11 &
it . 36
= 10 &
it . 37
= 13 &
it . 38
= 7 &
it . 39
= 8 &
it . 40
= 15 &
it . 41
= 9 &
it . 42
= 12 &
it . 43
= 5 &
it . 44
= 6 &
it . 45
= 3 &
it . 46
= 0 &
it . 47
= 14 &
it . 48
= 11 &
it . 49
= 8 &
it . 50
= 12 &
it . 51
= 7 &
it . 52
= 1 &
it . 53
= 14 &
it . 54
= 2 &
it . 55
= 13 &
it . 56
= 6 &
it . 57
= 15 &
it . 58
= 0 &
it . 59
= 9 &
it . 60
= 10 &
it . 61
= 4 &
it . 62
= 5 &
it . 63
= 3 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 2 & b1 . 1 = 12 & b1 . 2 = 4 & b1 . 3 = 1 & b1 . 4 = 7 & b1 . 5 = 10 & b1 . 6 = 11 & b1 . 7 = 6 & b1 . 8 = 8 & b1 . 9 = 5 & b1 . 10 = 3 & b1 . 11 = 15 & b1 . 12 = 13 & b1 . 13 = 0 & b1 . 14 = 14 & b1 . 15 = 9 & b1 . 16 = 14 & b1 . 17 = 11 & b1 . 18 = 2 & b1 . 19 = 12 & b1 . 20 = 4 & b1 . 21 = 7 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 5 & b1 . 25 = 0 & b1 . 26 = 15 & b1 . 27 = 10 & b1 . 28 = 3 & b1 . 29 = 9 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 4 & b1 . 33 = 2 & b1 . 34 = 1 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 13 & b1 . 38 = 7 & b1 . 39 = 8 & b1 . 40 = 15 & b1 . 41 = 9 & b1 . 42 = 12 & b1 . 43 = 5 & b1 . 44 = 6 & b1 . 45 = 3 & b1 . 46 = 0 & b1 . 47 = 14 & b1 . 48 = 11 & b1 . 49 = 8 & b1 . 50 = 12 & b1 . 51 = 7 & b1 . 52 = 1 & b1 . 53 = 14 & b1 . 54 = 2 & b1 . 55 = 13 & b1 . 56 = 6 & b1 . 57 = 15 & b1 . 58 = 0 & b1 . 59 = 9 & b1 . 60 = 10 & b1 . 61 = 4 & b1 . 62 = 5 & b1 . 63 = 3 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 2 & b1 . 1 = 12 & b1 . 2 = 4 & b1 . 3 = 1 & b1 . 4 = 7 & b1 . 5 = 10 & b1 . 6 = 11 & b1 . 7 = 6 & b1 . 8 = 8 & b1 . 9 = 5 & b1 . 10 = 3 & b1 . 11 = 15 & b1 . 12 = 13 & b1 . 13 = 0 & b1 . 14 = 14 & b1 . 15 = 9 & b1 . 16 = 14 & b1 . 17 = 11 & b1 . 18 = 2 & b1 . 19 = 12 & b1 . 20 = 4 & b1 . 21 = 7 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 5 & b1 . 25 = 0 & b1 . 26 = 15 & b1 . 27 = 10 & b1 . 28 = 3 & b1 . 29 = 9 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 4 & b1 . 33 = 2 & b1 . 34 = 1 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 13 & b1 . 38 = 7 & b1 . 39 = 8 & b1 . 40 = 15 & b1 . 41 = 9 & b1 . 42 = 12 & b1 . 43 = 5 & b1 . 44 = 6 & b1 . 45 = 3 & b1 . 46 = 0 & b1 . 47 = 14 & b1 . 48 = 11 & b1 . 49 = 8 & b1 . 50 = 12 & b1 . 51 = 7 & b1 . 52 = 1 & b1 . 53 = 14 & b1 . 54 = 2 & b1 . 55 = 13 & b1 . 56 = 6 & b1 . 57 = 15 & b1 . 58 = 0 & b1 . 59 = 9 & b1 . 60 = 10 & b1 . 61 = 4 & b1 . 62 = 5 & b1 . 63 = 3 & b2 . 0 = 2 & b2 . 1 = 12 & b2 . 2 = 4 & b2 . 3 = 1 & b2 . 4 = 7 & b2 . 5 = 10 & b2 . 6 = 11 & b2 . 7 = 6 & b2 . 8 = 8 & b2 . 9 = 5 & b2 . 10 = 3 & b2 . 11 = 15 & b2 . 12 = 13 & b2 . 13 = 0 & b2 . 14 = 14 & b2 . 15 = 9 & b2 . 16 = 14 & b2 . 17 = 11 & b2 . 18 = 2 & b2 . 19 = 12 & b2 . 20 = 4 & b2 . 21 = 7 & b2 . 22 = 13 & b2 . 23 = 1 & b2 . 24 = 5 & b2 . 25 = 0 & b2 . 26 = 15 & b2 . 27 = 10 & b2 . 28 = 3 & b2 . 29 = 9 & b2 . 30 = 8 & b2 . 31 = 6 & b2 . 32 = 4 & b2 . 33 = 2 & b2 . 34 = 1 & b2 . 35 = 11 & b2 . 36 = 10 & b2 . 37 = 13 & b2 . 38 = 7 & b2 . 39 = 8 & b2 . 40 = 15 & b2 . 41 = 9 & b2 . 42 = 12 & b2 . 43 = 5 & b2 . 44 = 6 & b2 . 45 = 3 & b2 . 46 = 0 & b2 . 47 = 14 & b2 . 48 = 11 & b2 . 49 = 8 & b2 . 50 = 12 & b2 . 51 = 7 & b2 . 52 = 1 & b2 . 53 = 14 & b2 . 54 = 2 & b2 . 55 = 13 & b2 . 56 = 6 & b2 . 57 = 15 & b2 . 58 = 0 & b2 . 59 = 9 & b2 . 60 = 10 & b2 . 61 = 4 & b2 . 62 = 5 & b2 . 63 = 3 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX5 DESCIP_1:def 10 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX5 iff ( b1 . 0 = 2 & b1 . 1 = 12 & b1 . 2 = 4 & b1 . 3 = 1 & b1 . 4 = 7 & b1 . 5 = 10 & b1 . 6 = 11 & b1 . 7 = 6 & b1 . 8 = 8 & b1 . 9 = 5 & b1 . 10 = 3 & b1 . 11 = 15 & b1 . 12 = 13 & b1 . 13 = 0 & b1 . 14 = 14 & b1 . 15 = 9 & b1 . 16 = 14 & b1 . 17 = 11 & b1 . 18 = 2 & b1 . 19 = 12 & b1 . 20 = 4 & b1 . 21 = 7 & b1 . 22 = 13 & b1 . 23 = 1 & b1 . 24 = 5 & b1 . 25 = 0 & b1 . 26 = 15 & b1 . 27 = 10 & b1 . 28 = 3 & b1 . 29 = 9 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 4 & b1 . 33 = 2 & b1 . 34 = 1 & b1 . 35 = 11 & b1 . 36 = 10 & b1 . 37 = 13 & b1 . 38 = 7 & b1 . 39 = 8 & b1 . 40 = 15 & b1 . 41 = 9 & b1 . 42 = 12 & b1 . 43 = 5 & b1 . 44 = 6 & b1 . 45 = 3 & b1 . 46 = 0 & b1 . 47 = 14 & b1 . 48 = 11 & b1 . 49 = 8 & b1 . 50 = 12 & b1 . 51 = 7 & b1 . 52 = 1 & b1 . 53 = 14 & b1 . 54 = 2 & b1 . 55 = 13 & b1 . 56 = 6 & b1 . 57 = 15 & b1 . 58 = 0 & b1 . 59 = 9 & b1 . 60 = 10 & b1 . 61 = 4 & b1 . 62 = 5 & b1 . 63 = 3 ) );
definition
func DES-SBOX6 -> Function of 64,16
means
(
it . 0 = 12 &
it . 1
= 1 &
it . 2
= 10 &
it . 3
= 15 &
it . 4
= 9 &
it . 5
= 2 &
it . 6
= 6 &
it . 7
= 8 &
it . 8
= 0 &
it . 9
= 13 &
it . 10
= 3 &
it . 11
= 4 &
it . 12
= 14 &
it . 13
= 7 &
it . 14
= 5 &
it . 15
= 11 &
it . 16
= 10 &
it . 17
= 15 &
it . 18
= 4 &
it . 19
= 2 &
it . 20
= 7 &
it . 21
= 12 &
it . 22
= 9 &
it . 23
= 5 &
it . 24
= 6 &
it . 25
= 1 &
it . 26
= 13 &
it . 27
= 14 &
it . 28
= 0 &
it . 29
= 11 &
it . 30
= 3 &
it . 31
= 8 &
it . 32
= 9 &
it . 33
= 14 &
it . 34
= 15 &
it . 35
= 5 &
it . 36
= 2 &
it . 37
= 8 &
it . 38
= 12 &
it . 39
= 3 &
it . 40
= 7 &
it . 41
= 0 &
it . 42
= 4 &
it . 43
= 10 &
it . 44
= 1 &
it . 45
= 13 &
it . 46
= 11 &
it . 47
= 6 &
it . 48
= 4 &
it . 49
= 3 &
it . 50
= 2 &
it . 51
= 12 &
it . 52
= 9 &
it . 53
= 5 &
it . 54
= 15 &
it . 55
= 10 &
it . 56
= 11 &
it . 57
= 14 &
it . 58
= 1 &
it . 59
= 7 &
it . 60
= 6 &
it . 61
= 0 &
it . 62
= 8 &
it . 63
= 13 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 12 & b1 . 1 = 1 & b1 . 2 = 10 & b1 . 3 = 15 & b1 . 4 = 9 & b1 . 5 = 2 & b1 . 6 = 6 & b1 . 7 = 8 & b1 . 8 = 0 & b1 . 9 = 13 & b1 . 10 = 3 & b1 . 11 = 4 & b1 . 12 = 14 & b1 . 13 = 7 & b1 . 14 = 5 & b1 . 15 = 11 & b1 . 16 = 10 & b1 . 17 = 15 & b1 . 18 = 4 & b1 . 19 = 2 & b1 . 20 = 7 & b1 . 21 = 12 & b1 . 22 = 9 & b1 . 23 = 5 & b1 . 24 = 6 & b1 . 25 = 1 & b1 . 26 = 13 & b1 . 27 = 14 & b1 . 28 = 0 & b1 . 29 = 11 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 9 & b1 . 33 = 14 & b1 . 34 = 15 & b1 . 35 = 5 & b1 . 36 = 2 & b1 . 37 = 8 & b1 . 38 = 12 & b1 . 39 = 3 & b1 . 40 = 7 & b1 . 41 = 0 & b1 . 42 = 4 & b1 . 43 = 10 & b1 . 44 = 1 & b1 . 45 = 13 & b1 . 46 = 11 & b1 . 47 = 6 & b1 . 48 = 4 & b1 . 49 = 3 & b1 . 50 = 2 & b1 . 51 = 12 & b1 . 52 = 9 & b1 . 53 = 5 & b1 . 54 = 15 & b1 . 55 = 10 & b1 . 56 = 11 & b1 . 57 = 14 & b1 . 58 = 1 & b1 . 59 = 7 & b1 . 60 = 6 & b1 . 61 = 0 & b1 . 62 = 8 & b1 . 63 = 13 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 12 & b1 . 1 = 1 & b1 . 2 = 10 & b1 . 3 = 15 & b1 . 4 = 9 & b1 . 5 = 2 & b1 . 6 = 6 & b1 . 7 = 8 & b1 . 8 = 0 & b1 . 9 = 13 & b1 . 10 = 3 & b1 . 11 = 4 & b1 . 12 = 14 & b1 . 13 = 7 & b1 . 14 = 5 & b1 . 15 = 11 & b1 . 16 = 10 & b1 . 17 = 15 & b1 . 18 = 4 & b1 . 19 = 2 & b1 . 20 = 7 & b1 . 21 = 12 & b1 . 22 = 9 & b1 . 23 = 5 & b1 . 24 = 6 & b1 . 25 = 1 & b1 . 26 = 13 & b1 . 27 = 14 & b1 . 28 = 0 & b1 . 29 = 11 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 9 & b1 . 33 = 14 & b1 . 34 = 15 & b1 . 35 = 5 & b1 . 36 = 2 & b1 . 37 = 8 & b1 . 38 = 12 & b1 . 39 = 3 & b1 . 40 = 7 & b1 . 41 = 0 & b1 . 42 = 4 & b1 . 43 = 10 & b1 . 44 = 1 & b1 . 45 = 13 & b1 . 46 = 11 & b1 . 47 = 6 & b1 . 48 = 4 & b1 . 49 = 3 & b1 . 50 = 2 & b1 . 51 = 12 & b1 . 52 = 9 & b1 . 53 = 5 & b1 . 54 = 15 & b1 . 55 = 10 & b1 . 56 = 11 & b1 . 57 = 14 & b1 . 58 = 1 & b1 . 59 = 7 & b1 . 60 = 6 & b1 . 61 = 0 & b1 . 62 = 8 & b1 . 63 = 13 & b2 . 0 = 12 & b2 . 1 = 1 & b2 . 2 = 10 & b2 . 3 = 15 & b2 . 4 = 9 & b2 . 5 = 2 & b2 . 6 = 6 & b2 . 7 = 8 & b2 . 8 = 0 & b2 . 9 = 13 & b2 . 10 = 3 & b2 . 11 = 4 & b2 . 12 = 14 & b2 . 13 = 7 & b2 . 14 = 5 & b2 . 15 = 11 & b2 . 16 = 10 & b2 . 17 = 15 & b2 . 18 = 4 & b2 . 19 = 2 & b2 . 20 = 7 & b2 . 21 = 12 & b2 . 22 = 9 & b2 . 23 = 5 & b2 . 24 = 6 & b2 . 25 = 1 & b2 . 26 = 13 & b2 . 27 = 14 & b2 . 28 = 0 & b2 . 29 = 11 & b2 . 30 = 3 & b2 . 31 = 8 & b2 . 32 = 9 & b2 . 33 = 14 & b2 . 34 = 15 & b2 . 35 = 5 & b2 . 36 = 2 & b2 . 37 = 8 & b2 . 38 = 12 & b2 . 39 = 3 & b2 . 40 = 7 & b2 . 41 = 0 & b2 . 42 = 4 & b2 . 43 = 10 & b2 . 44 = 1 & b2 . 45 = 13 & b2 . 46 = 11 & b2 . 47 = 6 & b2 . 48 = 4 & b2 . 49 = 3 & b2 . 50 = 2 & b2 . 51 = 12 & b2 . 52 = 9 & b2 . 53 = 5 & b2 . 54 = 15 & b2 . 55 = 10 & b2 . 56 = 11 & b2 . 57 = 14 & b2 . 58 = 1 & b2 . 59 = 7 & b2 . 60 = 6 & b2 . 61 = 0 & b2 . 62 = 8 & b2 . 63 = 13 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX6 DESCIP_1:def 11 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX6 iff ( b1 . 0 = 12 & b1 . 1 = 1 & b1 . 2 = 10 & b1 . 3 = 15 & b1 . 4 = 9 & b1 . 5 = 2 & b1 . 6 = 6 & b1 . 7 = 8 & b1 . 8 = 0 & b1 . 9 = 13 & b1 . 10 = 3 & b1 . 11 = 4 & b1 . 12 = 14 & b1 . 13 = 7 & b1 . 14 = 5 & b1 . 15 = 11 & b1 . 16 = 10 & b1 . 17 = 15 & b1 . 18 = 4 & b1 . 19 = 2 & b1 . 20 = 7 & b1 . 21 = 12 & b1 . 22 = 9 & b1 . 23 = 5 & b1 . 24 = 6 & b1 . 25 = 1 & b1 . 26 = 13 & b1 . 27 = 14 & b1 . 28 = 0 & b1 . 29 = 11 & b1 . 30 = 3 & b1 . 31 = 8 & b1 . 32 = 9 & b1 . 33 = 14 & b1 . 34 = 15 & b1 . 35 = 5 & b1 . 36 = 2 & b1 . 37 = 8 & b1 . 38 = 12 & b1 . 39 = 3 & b1 . 40 = 7 & b1 . 41 = 0 & b1 . 42 = 4 & b1 . 43 = 10 & b1 . 44 = 1 & b1 . 45 = 13 & b1 . 46 = 11 & b1 . 47 = 6 & b1 . 48 = 4 & b1 . 49 = 3 & b1 . 50 = 2 & b1 . 51 = 12 & b1 . 52 = 9 & b1 . 53 = 5 & b1 . 54 = 15 & b1 . 55 = 10 & b1 . 56 = 11 & b1 . 57 = 14 & b1 . 58 = 1 & b1 . 59 = 7 & b1 . 60 = 6 & b1 . 61 = 0 & b1 . 62 = 8 & b1 . 63 = 13 ) );
definition
func DES-SBOX7 -> Function of 64,16
means
(
it . 0 = 4 &
it . 1
= 11 &
it . 2
= 2 &
it . 3
= 14 &
it . 4
= 15 &
it . 5
= 0 &
it . 6
= 8 &
it . 7
= 13 &
it . 8
= 3 &
it . 9
= 12 &
it . 10
= 9 &
it . 11
= 7 &
it . 12
= 5 &
it . 13
= 10 &
it . 14
= 6 &
it . 15
= 1 &
it . 16
= 13 &
it . 17
= 0 &
it . 18
= 11 &
it . 19
= 7 &
it . 20
= 4 &
it . 21
= 9 &
it . 22
= 1 &
it . 23
= 10 &
it . 24
= 14 &
it . 25
= 3 &
it . 26
= 5 &
it . 27
= 12 &
it . 28
= 2 &
it . 29
= 15 &
it . 30
= 8 &
it . 31
= 6 &
it . 32
= 1 &
it . 33
= 4 &
it . 34
= 11 &
it . 35
= 13 &
it . 36
= 12 &
it . 37
= 3 &
it . 38
= 7 &
it . 39
= 14 &
it . 40
= 10 &
it . 41
= 15 &
it . 42
= 6 &
it . 43
= 8 &
it . 44
= 0 &
it . 45
= 5 &
it . 46
= 9 &
it . 47
= 2 &
it . 48
= 6 &
it . 49
= 11 &
it . 50
= 13 &
it . 51
= 8 &
it . 52
= 1 &
it . 53
= 4 &
it . 54
= 10 &
it . 55
= 7 &
it . 56
= 9 &
it . 57
= 5 &
it . 58
= 0 &
it . 59
= 15 &
it . 60
= 14 &
it . 61
= 2 &
it . 62
= 3 &
it . 63
= 12 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 4 & b1 . 1 = 11 & b1 . 2 = 2 & b1 . 3 = 14 & b1 . 4 = 15 & b1 . 5 = 0 & b1 . 6 = 8 & b1 . 7 = 13 & b1 . 8 = 3 & b1 . 9 = 12 & b1 . 10 = 9 & b1 . 11 = 7 & b1 . 12 = 5 & b1 . 13 = 10 & b1 . 14 = 6 & b1 . 15 = 1 & b1 . 16 = 13 & b1 . 17 = 0 & b1 . 18 = 11 & b1 . 19 = 7 & b1 . 20 = 4 & b1 . 21 = 9 & b1 . 22 = 1 & b1 . 23 = 10 & b1 . 24 = 14 & b1 . 25 = 3 & b1 . 26 = 5 & b1 . 27 = 12 & b1 . 28 = 2 & b1 . 29 = 15 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 1 & b1 . 33 = 4 & b1 . 34 = 11 & b1 . 35 = 13 & b1 . 36 = 12 & b1 . 37 = 3 & b1 . 38 = 7 & b1 . 39 = 14 & b1 . 40 = 10 & b1 . 41 = 15 & b1 . 42 = 6 & b1 . 43 = 8 & b1 . 44 = 0 & b1 . 45 = 5 & b1 . 46 = 9 & b1 . 47 = 2 & b1 . 48 = 6 & b1 . 49 = 11 & b1 . 50 = 13 & b1 . 51 = 8 & b1 . 52 = 1 & b1 . 53 = 4 & b1 . 54 = 10 & b1 . 55 = 7 & b1 . 56 = 9 & b1 . 57 = 5 & b1 . 58 = 0 & b1 . 59 = 15 & b1 . 60 = 14 & b1 . 61 = 2 & b1 . 62 = 3 & b1 . 63 = 12 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 4 & b1 . 1 = 11 & b1 . 2 = 2 & b1 . 3 = 14 & b1 . 4 = 15 & b1 . 5 = 0 & b1 . 6 = 8 & b1 . 7 = 13 & b1 . 8 = 3 & b1 . 9 = 12 & b1 . 10 = 9 & b1 . 11 = 7 & b1 . 12 = 5 & b1 . 13 = 10 & b1 . 14 = 6 & b1 . 15 = 1 & b1 . 16 = 13 & b1 . 17 = 0 & b1 . 18 = 11 & b1 . 19 = 7 & b1 . 20 = 4 & b1 . 21 = 9 & b1 . 22 = 1 & b1 . 23 = 10 & b1 . 24 = 14 & b1 . 25 = 3 & b1 . 26 = 5 & b1 . 27 = 12 & b1 . 28 = 2 & b1 . 29 = 15 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 1 & b1 . 33 = 4 & b1 . 34 = 11 & b1 . 35 = 13 & b1 . 36 = 12 & b1 . 37 = 3 & b1 . 38 = 7 & b1 . 39 = 14 & b1 . 40 = 10 & b1 . 41 = 15 & b1 . 42 = 6 & b1 . 43 = 8 & b1 . 44 = 0 & b1 . 45 = 5 & b1 . 46 = 9 & b1 . 47 = 2 & b1 . 48 = 6 & b1 . 49 = 11 & b1 . 50 = 13 & b1 . 51 = 8 & b1 . 52 = 1 & b1 . 53 = 4 & b1 . 54 = 10 & b1 . 55 = 7 & b1 . 56 = 9 & b1 . 57 = 5 & b1 . 58 = 0 & b1 . 59 = 15 & b1 . 60 = 14 & b1 . 61 = 2 & b1 . 62 = 3 & b1 . 63 = 12 & b2 . 0 = 4 & b2 . 1 = 11 & b2 . 2 = 2 & b2 . 3 = 14 & b2 . 4 = 15 & b2 . 5 = 0 & b2 . 6 = 8 & b2 . 7 = 13 & b2 . 8 = 3 & b2 . 9 = 12 & b2 . 10 = 9 & b2 . 11 = 7 & b2 . 12 = 5 & b2 . 13 = 10 & b2 . 14 = 6 & b2 . 15 = 1 & b2 . 16 = 13 & b2 . 17 = 0 & b2 . 18 = 11 & b2 . 19 = 7 & b2 . 20 = 4 & b2 . 21 = 9 & b2 . 22 = 1 & b2 . 23 = 10 & b2 . 24 = 14 & b2 . 25 = 3 & b2 . 26 = 5 & b2 . 27 = 12 & b2 . 28 = 2 & b2 . 29 = 15 & b2 . 30 = 8 & b2 . 31 = 6 & b2 . 32 = 1 & b2 . 33 = 4 & b2 . 34 = 11 & b2 . 35 = 13 & b2 . 36 = 12 & b2 . 37 = 3 & b2 . 38 = 7 & b2 . 39 = 14 & b2 . 40 = 10 & b2 . 41 = 15 & b2 . 42 = 6 & b2 . 43 = 8 & b2 . 44 = 0 & b2 . 45 = 5 & b2 . 46 = 9 & b2 . 47 = 2 & b2 . 48 = 6 & b2 . 49 = 11 & b2 . 50 = 13 & b2 . 51 = 8 & b2 . 52 = 1 & b2 . 53 = 4 & b2 . 54 = 10 & b2 . 55 = 7 & b2 . 56 = 9 & b2 . 57 = 5 & b2 . 58 = 0 & b2 . 59 = 15 & b2 . 60 = 14 & b2 . 61 = 2 & b2 . 62 = 3 & b2 . 63 = 12 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX7 DESCIP_1:def 12 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX7 iff ( b1 . 0 = 4 & b1 . 1 = 11 & b1 . 2 = 2 & b1 . 3 = 14 & b1 . 4 = 15 & b1 . 5 = 0 & b1 . 6 = 8 & b1 . 7 = 13 & b1 . 8 = 3 & b1 . 9 = 12 & b1 . 10 = 9 & b1 . 11 = 7 & b1 . 12 = 5 & b1 . 13 = 10 & b1 . 14 = 6 & b1 . 15 = 1 & b1 . 16 = 13 & b1 . 17 = 0 & b1 . 18 = 11 & b1 . 19 = 7 & b1 . 20 = 4 & b1 . 21 = 9 & b1 . 22 = 1 & b1 . 23 = 10 & b1 . 24 = 14 & b1 . 25 = 3 & b1 . 26 = 5 & b1 . 27 = 12 & b1 . 28 = 2 & b1 . 29 = 15 & b1 . 30 = 8 & b1 . 31 = 6 & b1 . 32 = 1 & b1 . 33 = 4 & b1 . 34 = 11 & b1 . 35 = 13 & b1 . 36 = 12 & b1 . 37 = 3 & b1 . 38 = 7 & b1 . 39 = 14 & b1 . 40 = 10 & b1 . 41 = 15 & b1 . 42 = 6 & b1 . 43 = 8 & b1 . 44 = 0 & b1 . 45 = 5 & b1 . 46 = 9 & b1 . 47 = 2 & b1 . 48 = 6 & b1 . 49 = 11 & b1 . 50 = 13 & b1 . 51 = 8 & b1 . 52 = 1 & b1 . 53 = 4 & b1 . 54 = 10 & b1 . 55 = 7 & b1 . 56 = 9 & b1 . 57 = 5 & b1 . 58 = 0 & b1 . 59 = 15 & b1 . 60 = 14 & b1 . 61 = 2 & b1 . 62 = 3 & b1 . 63 = 12 ) );
definition
func DES-SBOX8 -> Function of 64,16
means
(
it . 0 = 13 &
it . 1
= 2 &
it . 2
= 8 &
it . 3
= 4 &
it . 4
= 6 &
it . 5
= 15 &
it . 6
= 11 &
it . 7
= 1 &
it . 8
= 10 &
it . 9
= 9 &
it . 10
= 3 &
it . 11
= 14 &
it . 12
= 5 &
it . 13
= 0 &
it . 14
= 12 &
it . 15
= 7 &
it . 16
= 1 &
it . 17
= 15 &
it . 18
= 13 &
it . 19
= 8 &
it . 20
= 10 &
it . 21
= 3 &
it . 22
= 7 &
it . 23
= 4 &
it . 24
= 12 &
it . 25
= 5 &
it . 26
= 5 &
it . 27
= 11 &
it . 28
= 0 &
it . 29
= 14 &
it . 30
= 9 &
it . 31
= 2 &
it . 32
= 7 &
it . 33
= 11 &
it . 34
= 4 &
it . 35
= 1 &
it . 36
= 9 &
it . 37
= 12 &
it . 38
= 14 &
it . 39
= 2 &
it . 40
= 0 &
it . 41
= 6 &
it . 42
= 10 &
it . 43
= 13 &
it . 44
= 15 &
it . 45
= 3 &
it . 46
= 5 &
it . 47
= 8 &
it . 48
= 2 &
it . 49
= 1 &
it . 50
= 14 &
it . 51
= 7 &
it . 52
= 4 &
it . 53
= 10 &
it . 54
= 8 &
it . 55
= 13 &
it . 56
= 15 &
it . 57
= 12 &
it . 58
= 9 &
it . 59
= 0 &
it . 60
= 3 &
it . 61
= 5 &
it . 62
= 6 &
it . 63
= 11 );
existence
ex b1 being Function of 64,16 st
( b1 . 0 = 13 & b1 . 1 = 2 & b1 . 2 = 8 & b1 . 3 = 4 & b1 . 4 = 6 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 1 & b1 . 8 = 10 & b1 . 9 = 9 & b1 . 10 = 3 & b1 . 11 = 14 & b1 . 12 = 5 & b1 . 13 = 0 & b1 . 14 = 12 & b1 . 15 = 7 & b1 . 16 = 1 & b1 . 17 = 15 & b1 . 18 = 13 & b1 . 19 = 8 & b1 . 20 = 10 & b1 . 21 = 3 & b1 . 22 = 7 & b1 . 23 = 4 & b1 . 24 = 12 & b1 . 25 = 5 & b1 . 26 = 5 & b1 . 27 = 11 & b1 . 28 = 0 & b1 . 29 = 14 & b1 . 30 = 9 & b1 . 31 = 2 & b1 . 32 = 7 & b1 . 33 = 11 & b1 . 34 = 4 & b1 . 35 = 1 & b1 . 36 = 9 & b1 . 37 = 12 & b1 . 38 = 14 & b1 . 39 = 2 & b1 . 40 = 0 & b1 . 41 = 6 & b1 . 42 = 10 & b1 . 43 = 13 & b1 . 44 = 15 & b1 . 45 = 3 & b1 . 46 = 5 & b1 . 47 = 8 & b1 . 48 = 2 & b1 . 49 = 1 & b1 . 50 = 14 & b1 . 51 = 7 & b1 . 52 = 4 & b1 . 53 = 10 & b1 . 54 = 8 & b1 . 55 = 13 & b1 . 56 = 15 & b1 . 57 = 12 & b1 . 58 = 9 & b1 . 59 = 0 & b1 . 60 = 3 & b1 . 61 = 5 & b1 . 62 = 6 & b1 . 63 = 11 )
by Th27, Lm3;
uniqueness
for b1, b2 being Function of 64,16 st b1 . 0 = 13 & b1 . 1 = 2 & b1 . 2 = 8 & b1 . 3 = 4 & b1 . 4 = 6 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 1 & b1 . 8 = 10 & b1 . 9 = 9 & b1 . 10 = 3 & b1 . 11 = 14 & b1 . 12 = 5 & b1 . 13 = 0 & b1 . 14 = 12 & b1 . 15 = 7 & b1 . 16 = 1 & b1 . 17 = 15 & b1 . 18 = 13 & b1 . 19 = 8 & b1 . 20 = 10 & b1 . 21 = 3 & b1 . 22 = 7 & b1 . 23 = 4 & b1 . 24 = 12 & b1 . 25 = 5 & b1 . 26 = 5 & b1 . 27 = 11 & b1 . 28 = 0 & b1 . 29 = 14 & b1 . 30 = 9 & b1 . 31 = 2 & b1 . 32 = 7 & b1 . 33 = 11 & b1 . 34 = 4 & b1 . 35 = 1 & b1 . 36 = 9 & b1 . 37 = 12 & b1 . 38 = 14 & b1 . 39 = 2 & b1 . 40 = 0 & b1 . 41 = 6 & b1 . 42 = 10 & b1 . 43 = 13 & b1 . 44 = 15 & b1 . 45 = 3 & b1 . 46 = 5 & b1 . 47 = 8 & b1 . 48 = 2 & b1 . 49 = 1 & b1 . 50 = 14 & b1 . 51 = 7 & b1 . 52 = 4 & b1 . 53 = 10 & b1 . 54 = 8 & b1 . 55 = 13 & b1 . 56 = 15 & b1 . 57 = 12 & b1 . 58 = 9 & b1 . 59 = 0 & b1 . 60 = 3 & b1 . 61 = 5 & b1 . 62 = 6 & b1 . 63 = 11 & b2 . 0 = 13 & b2 . 1 = 2 & b2 . 2 = 8 & b2 . 3 = 4 & b2 . 4 = 6 & b2 . 5 = 15 & b2 . 6 = 11 & b2 . 7 = 1 & b2 . 8 = 10 & b2 . 9 = 9 & b2 . 10 = 3 & b2 . 11 = 14 & b2 . 12 = 5 & b2 . 13 = 0 & b2 . 14 = 12 & b2 . 15 = 7 & b2 . 16 = 1 & b2 . 17 = 15 & b2 . 18 = 13 & b2 . 19 = 8 & b2 . 20 = 10 & b2 . 21 = 3 & b2 . 22 = 7 & b2 . 23 = 4 & b2 . 24 = 12 & b2 . 25 = 5 & b2 . 26 = 5 & b2 . 27 = 11 & b2 . 28 = 0 & b2 . 29 = 14 & b2 . 30 = 9 & b2 . 31 = 2 & b2 . 32 = 7 & b2 . 33 = 11 & b2 . 34 = 4 & b2 . 35 = 1 & b2 . 36 = 9 & b2 . 37 = 12 & b2 . 38 = 14 & b2 . 39 = 2 & b2 . 40 = 0 & b2 . 41 = 6 & b2 . 42 = 10 & b2 . 43 = 13 & b2 . 44 = 15 & b2 . 45 = 3 & b2 . 46 = 5 & b2 . 47 = 8 & b2 . 48 = 2 & b2 . 49 = 1 & b2 . 50 = 14 & b2 . 51 = 7 & b2 . 52 = 4 & b2 . 53 = 10 & b2 . 54 = 8 & b2 . 55 = 13 & b2 . 56 = 15 & b2 . 57 = 12 & b2 . 58 = 9 & b2 . 59 = 0 & b2 . 60 = 3 & b2 . 61 = 5 & b2 . 62 = 6 & b2 . 63 = 11 holds
b1 = b2
by Lm4;
end;
::
deftheorem defines
DES-SBOX8 DESCIP_1:def 13 :
for b1 being Function of 64,16 holds
( b1 = DES-SBOX8 iff ( b1 . 0 = 13 & b1 . 1 = 2 & b1 . 2 = 8 & b1 . 3 = 4 & b1 . 4 = 6 & b1 . 5 = 15 & b1 . 6 = 11 & b1 . 7 = 1 & b1 . 8 = 10 & b1 . 9 = 9 & b1 . 10 = 3 & b1 . 11 = 14 & b1 . 12 = 5 & b1 . 13 = 0 & b1 . 14 = 12 & b1 . 15 = 7 & b1 . 16 = 1 & b1 . 17 = 15 & b1 . 18 = 13 & b1 . 19 = 8 & b1 . 20 = 10 & b1 . 21 = 3 & b1 . 22 = 7 & b1 . 23 = 4 & b1 . 24 = 12 & b1 . 25 = 5 & b1 . 26 = 5 & b1 . 27 = 11 & b1 . 28 = 0 & b1 . 29 = 14 & b1 . 30 = 9 & b1 . 31 = 2 & b1 . 32 = 7 & b1 . 33 = 11 & b1 . 34 = 4 & b1 . 35 = 1 & b1 . 36 = 9 & b1 . 37 = 12 & b1 . 38 = 14 & b1 . 39 = 2 & b1 . 40 = 0 & b1 . 41 = 6 & b1 . 42 = 10 & b1 . 43 = 13 & b1 . 44 = 15 & b1 . 45 = 3 & b1 . 46 = 5 & b1 . 47 = 8 & b1 . 48 = 2 & b1 . 49 = 1 & b1 . 50 = 14 & b1 . 51 = 7 & b1 . 52 = 4 & b1 . 53 = 10 & b1 . 54 = 8 & b1 . 55 = 13 & b1 . 56 = 15 & b1 . 57 = 12 & b1 . 58 = 9 & b1 . 59 = 0 & b1 . 60 = 3 & b1 . 61 = 5 & b1 . 62 = 6 & b1 . 63 = 11 ) );
definition
let r be
Element of 64
-tuples_on BOOLEAN;
func DES-IP r -> Element of 64
-tuples_on BOOLEAN means :
Def14:
(
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 )
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
end;
::
deftheorem Def14 defines
DES-IP DESCIP_1:def 14 :
for r, b2 being Element of 64 -tuples_on BOOLEAN holds
( b2 = DES-IP r iff ( b2 . 1 = r . 58 & b2 . 2 = r . 50 & b2 . 3 = r . 42 & b2 . 4 = r . 34 & b2 . 5 = r . 26 & b2 . 6 = r . 18 & b2 . 7 = r . 10 & b2 . 8 = r . 2 & b2 . 9 = r . 60 & b2 . 10 = r . 52 & b2 . 11 = r . 44 & b2 . 12 = r . 36 & b2 . 13 = r . 28 & b2 . 14 = r . 20 & b2 . 15 = r . 12 & b2 . 16 = r . 4 & b2 . 17 = r . 62 & b2 . 18 = r . 54 & b2 . 19 = r . 46 & b2 . 20 = r . 38 & b2 . 21 = r . 30 & b2 . 22 = r . 22 & b2 . 23 = r . 14 & b2 . 24 = r . 6 & b2 . 25 = r . 64 & b2 . 26 = r . 56 & b2 . 27 = r . 48 & b2 . 28 = r . 40 & b2 . 29 = r . 32 & b2 . 30 = r . 24 & b2 . 31 = r . 16 & b2 . 32 = r . 8 & b2 . 33 = r . 57 & b2 . 34 = r . 49 & b2 . 35 = r . 41 & b2 . 36 = r . 33 & b2 . 37 = r . 25 & b2 . 38 = r . 17 & b2 . 39 = r . 9 & b2 . 40 = r . 1 & b2 . 41 = r . 59 & b2 . 42 = r . 51 & b2 . 43 = r . 43 & b2 . 44 = r . 35 & b2 . 45 = r . 27 & b2 . 46 = r . 19 & b2 . 47 = r . 11 & b2 . 48 = r . 3 & b2 . 49 = r . 61 & b2 . 50 = r . 53 & b2 . 51 = r . 45 & b2 . 52 = r . 37 & b2 . 53 = r . 29 & b2 . 54 = r . 21 & b2 . 55 = r . 13 & b2 . 56 = r . 5 & b2 . 57 = r . 63 & b2 . 58 = r . 55 & b2 . 59 = r . 47 & b2 . 60 = r . 39 & b2 . 61 = r . 31 & b2 . 62 = r . 23 & b2 . 63 = r . 15 & b2 . 64 = r . 7 ) );
definition
let r be
Element of 64
-tuples_on BOOLEAN;
func DES-IPINV r -> Element of 64
-tuples_on BOOLEAN means :
Def16:
(
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 )
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
end;
::
deftheorem Def16 defines
DES-IPINV DESCIP_1:def 16 :
for r, b2 being Element of 64 -tuples_on BOOLEAN holds
( b2 = DES-IPINV r iff ( b2 . 1 = r . 40 & b2 . 2 = r . 8 & b2 . 3 = r . 48 & b2 . 4 = r . 16 & b2 . 5 = r . 56 & b2 . 6 = r . 24 & b2 . 7 = r . 64 & b2 . 8 = r . 32 & b2 . 9 = r . 39 & b2 . 10 = r . 7 & b2 . 11 = r . 47 & b2 . 12 = r . 15 & b2 . 13 = r . 55 & b2 . 14 = r . 23 & b2 . 15 = r . 63 & b2 . 16 = r . 31 & b2 . 17 = r . 38 & b2 . 18 = r . 6 & b2 . 19 = r . 46 & b2 . 20 = r . 14 & b2 . 21 = r . 54 & b2 . 22 = r . 22 & b2 . 23 = r . 62 & b2 . 24 = r . 30 & b2 . 25 = r . 37 & b2 . 26 = r . 5 & b2 . 27 = r . 45 & b2 . 28 = r . 13 & b2 . 29 = r . 53 & b2 . 30 = r . 21 & b2 . 31 = r . 61 & b2 . 32 = r . 29 & b2 . 33 = r . 36 & b2 . 34 = r . 4 & b2 . 35 = r . 44 & b2 . 36 = r . 12 & b2 . 37 = r . 52 & b2 . 38 = r . 20 & b2 . 39 = r . 60 & b2 . 40 = r . 28 & b2 . 41 = r . 35 & b2 . 42 = r . 3 & b2 . 43 = r . 43 & b2 . 44 = r . 11 & b2 . 45 = r . 51 & b2 . 46 = r . 19 & b2 . 47 = r . 59 & b2 . 48 = r . 27 & b2 . 49 = r . 34 & b2 . 50 = r . 2 & b2 . 51 = r . 42 & b2 . 52 = r . 10 & b2 . 53 = r . 50 & b2 . 54 = r . 18 & b2 . 55 = r . 58 & b2 . 56 = r . 26 & b2 . 57 = r . 33 & b2 . 58 = r . 1 & b2 . 59 = r . 41 & b2 . 60 = r . 9 & b2 . 61 = r . 49 & b2 . 62 = r . 17 & b2 . 63 = r . 57 & b2 . 64 = r . 25 ) );
Lm5:
for x being Element of 64 -tuples_on BOOLEAN holds DES-IPINV (DES-IP x) = x
Lm6:
for x being Element of 64 -tuples_on BOOLEAN holds DES-IP (DES-IPINV x) = x
Lm7:
DES-PIPINV * DES-PIP = id (64 -tuples_on BOOLEAN)
Lm8:
DES-PIP * DES-PIPINV = id (64 -tuples_on BOOLEAN)
definition
let r be
Element of 32
-tuples_on BOOLEAN;
func DES-E r -> Element of 48
-tuples_on BOOLEAN means
(
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 )
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
end;
definition
let r be
Element of 32
-tuples_on BOOLEAN;
func DES-P r -> Element of 32
-tuples_on BOOLEAN means
(
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 )
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
end;
definition
let r be
Element of 48
-tuples_on BOOLEAN;
func DES-DIV8 r -> Element of 8
-tuples_on (6 -tuples_on BOOLEAN) means :
Def20:
(
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) )
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
end;
::
deftheorem Def20 defines
DES-DIV8 DESCIP_1:def 20 :
for r being Element of 48 -tuples_on BOOLEAN
for b2 being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) holds
( b2 = DES-DIV8 r iff ( b2 . 1 = Op-Left (r,6) & b2 . 2 = Op-Left ((Op-Right (r,6)),6) & b2 . 3 = Op-Left ((Op-Right (r,12)),6) & b2 . 4 = Op-Left ((Op-Right (r,18)),6) & b2 . 5 = Op-Left ((Op-Right (r,24)),6) & b2 . 6 = Op-Left ((Op-Right (r,30)),6) & b2 . 7 = Op-Left ((Op-Right (r,36)),6) & b2 . 8 = Op-Right (r,42) ) );
Lm9:
for n being Nat
for b being Element of BOOLEAN holds n * b <= n