:: Formalization of the Data Encryption Standard
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received November 30, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DESCIP_1, TARSKI, XBOOLE_0, FINSEQ_1, RELAT_1, FUNCT_1, FUNCT_2,
FINSEQ_2, NAT_1, XBOOLEAN, MARGREL1, MCART_1, RFINSEQ, ZFMISC_1,
SUBSET_1, NUMBERS, INT_1, CARD_1, ARYTM_1, XXREAL_0, PARTFUN1, ARYTM_3,
ORDINAL4, ORDINAL1, FINSEQ_5, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1,
CARD_1, XTUPLE_0, DOMAIN_1, RELSET_1, PARTFUN1, BINOP_1, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1, FINSEQ_2, XBOOLEAN, MARGREL1,
FINSEQ_4, RFINSEQ, FINSEQ_5, BINARITH, BVFUNC_1, FUNCT_2;
constructors CARD_1, ENUMSET1, RELSET_1, BINOP_1, ARYTM_0, XXREAL_0, DOMAIN_1,
REAL_1, FINSEQ_4, RFUNCT_1, RFINSEQ, FINSEQ_5, BINARITH, NAT_D, BVFUNC_1;
registrations XREAL_0, RELSET_1, FINSEQ_2, FUNCT_2, ORDINAL1, MEMBERED,
XBOOLEAN, MARGREL1, INT_1, SUBSET_1, FINSEQ_1, NAT_1, XXREAL_0, XBOOLE_0,
VALUED_0, FINSEQ_4, XTUPLE_0, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions CARD_1, FUNCT_1, FUNCT_2, MARGREL1;
equalities XCMPLX_0, FINSEQ_1, FINSEQ_2, MARGREL1, ORDINAL1;
expansions CARD_1, FUNCT_1, FUNCT_2;
theorems NAT_D, TARSKI, ENUMSET1, RELAT_1, FUNCT_1, PARTFUN1, CARD_1, FUNCT_2,
XXREAL_0, XREAL_1, BVFUNC_1, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, XBOOLEAN,
FINSEQ_3, FINSEQ_4, RFINSEQ, FINSEQ_5, XBOOLE_0, XBOOLE_1, ORDINAL1;
schemes FUNCT_2, FINSEQ_1, NAT_1, RECDEF_2;
begin :: Preliminaries
reserve D for non empty set;
reserve s for FinSequence of D;
reserve m,n for Element of NAT;
registration
let n be Nat, f be n-element FinSequence;
cluster Rev f -> n-element;
coherence
proof
len f = n by CARD_1:def 7;
hence len Rev f = n by FINSEQ_5:def 3;
end;
end;
definition
let D be non empty set, n be Nat, f be Element of n-tuples_on D;
redefine func Rev f -> Element of n-tuples_on D; :: redefines Rev (FINSEQ_5, definition)
coherence
proof
len Rev(f) = n by CARD_1:def 7;
hence thesis by FINSEQ_2:92;
end;
end;
notation
let n be Nat, 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, n be Nat, f be FinSequence of D;
redefine func Op-Left(f,n) -> FinSequence of D; :: redefines Op-Left (DESCIP_1, synonym) → | (FINSEQ_1, definition)
coherence
proof
Op-Left(f,n) = f|n;
hence thesis;
end;
redefine func Op-Right(f,n) -> FinSequence of D; :: redefines Op-Right (DESCIP_1, synonym) → /^ (RFINSEQ, definition)
coherence
proof
Op-Right(f,n) = f/^n;
hence thesis;
end;
end;
notation
let D be non empty set, n be Nat, s be Element of (2*n)-tuples_on D;
synonym SP-Left↑(s) for Op-Left(s,n);
synonym SP-Right↑(s) for Op-Right(s,n);
end;
definition
let D be non empty set, n be Nat, s be Element of (2*n)-tuples_on D;
redefine func SP-Left(s) -> Element of n-tuples_on D; :: redefines SP-Left (DESCIP_1, synonym) → Op-Left (DESCIP_1, synonym) → | (FINSEQ_1, definition)
coherence
proof
A1: 1*n <= 2*n by XREAL_1:68;
len s = 2*n by CARD_1:def 7;then
len (Op-Left(s,n)) = n by A1,FINSEQ_1:59;
hence thesis by FINSEQ_2:92;
end;
end;
theorem Th1:
for m,n be non zero Element of NAT, s be Element of n-tuples_on D
st m <= n
holds Op-Left(s,m) is Element of m-tuples_on D
proof
let m,n be non zero Element of NAT,
s be Element of n-tuples_on D;
assume A1: m <= n;
len s = n by CARD_1:def 7;
then len (Op-Left(s,m)) = m by A1,FINSEQ_1:59;
then Op-Left(s,m) is Tuple of m,D by CARD_1:def 7;
hence thesis by FINSEQ_2:131;
end;
theorem Th2:
for m,n,l be non zero Element of NAT,
s be Element of n-tuples_on D
st m <= n & l= n - m
holds (Op-Right(s,m)) is Element of l-tuples_on D
proof
let m,n,l be non zero Element of NAT,
s be Element of n-tuples_on D;
assume A1: m <= n & l= n - m;
len s = n by CARD_1:def 7;
then len (Op-Right(s,m)) = l by A1,RFINSEQ:def 1;
then Op-Right(s,m) is Tuple of l,D by CARD_1:def 7;
hence thesis by FINSEQ_2:131;
end;
definition
let D be non empty set,n be non zero Element of NAT,
s be Element of (2*n)-tuples_on D;
redefine func SP-Right(s) -> Element of n-tuples_on D; :: redefines SP-Right (DESCIP_1, synonym) → Op-Right (DESCIP_1, synonym) → /^ (RFINSEQ, definition)
coherence
proof
A1:2*n -n =n;
1*n < 2*n by XREAL_1:68;
hence thesis by A1,Th2;
end;
end;
theorem Th3:
for n be non zero Element of NAT,
s be 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
(s /^1) ^ <* s.1 *>;
coherence;
end;
theorem Th4:
for s be FinSequence st 1 <= len s
holds len (Op-LeftShift(s)) = len s
proof
let s be FinSequence;
assume A1: 1 <= len s;
A2: len <* s.1 *> = 1 by FINSEQ_1:40;
len (s /^1) = (len s) - 1 by A1,RFINSEQ:def 1;
then
len ((s /^1) ^ <* s.1 *>) = ((len s) - 1) + 1 by A2,FINSEQ_1:22
.= (len s);
hence thesis;
end;
theorem Th5:
1 <= len s implies
Op-LeftShift(s) is FinSequence of D &
len (Op-LeftShift(s)) = len s
proof
assume A1: 1 <= len s;
then 1 in Seg (len s);
then 1 in dom s by FINSEQ_1:def 3;
then s.1 is Element of D by FINSEQ_2:11;
then s /^1 is FinSequence of D & <* s.1 *> is FinSequence of D
by FINSEQ_1:74;
hence thesis by Th4,A1,FINSEQ_1:75;
end;
theorem
for n be non zero Element of NAT,
s be Element of n-tuples_on D
holds (Op-LeftShift(s)) is Element of n-tuples_on D
proof
let n be non zero Element of NAT,
s be Element of n-tuples_on D;
A1: len s = n by CARD_1:def 7;
1 <= len s by NAT_1:14;
then (Op-LeftShift(s)) is FinSequence of D &
len (Op-LeftShift(s)) = len s by Th5;
then Op-LeftShift(s) is Tuple of n,D by A1,CARD_1:def 7;
hence thesis by FINSEQ_2:131;
end;
definition
let s be FinSequence;
func Op-RightShift(s) -> FinSequence equals
(<* s.(len s) *> ^ s )| len s;
coherence;
end;
theorem Th7:
for s be FinSequence holds len (Op-RightShift(s)) = len s
proof
let s be FinSequence;
A1: len <* s.(len s) *> = 1 by FINSEQ_1:40;
len ((<* s.(len s) *>) ^ s ) = (len s) + 1
by A1,FINSEQ_1:22;
hence thesis by FINSEQ_1:59,NAT_1:12;
end;
theorem Th8:
1 <= len s implies
Op-RightShift(s) is FinSequence of D
proof
assume 1 <= len s;
then len s in Seg (len s);
then len s in dom s by FINSEQ_1:def 3;
then s.(len s) is Element of D by FINSEQ_2:11;
then <* s.(len s) *> is FinSequence of D by FINSEQ_1:74;
then reconsider ss=((<* s.(len s) *>) ^ s )
as FinSequence of D by FINSEQ_1:75;
ss | (len s) is FinSequence of D;
hence thesis;
end;
theorem
for n be non zero Element of NAT,
s be Element of n-tuples_on D
holds (Op-RightShift(s)) is Element of n-tuples_on D
proof
let n be non zero Element of NAT,
s be Element of n-tuples_on D;
A1: len s = n by CARD_1:def 7;
(Op-RightShift(s)) is FinSequence of D &
len (Op-RightShift(s)) = len s by Th8,Th7,NAT_1:14;
then Op-RightShift(s) is Tuple of n,D by A1,CARD_1:def 7;
hence thesis by FINSEQ_2:131;
end;
definition
let D be non empty set;
let s be FinSequence of D,n be Integer;
assume A1: 1 <= len s;
func Op-Shift(s,n) -> FinSequence of D means
:Def3:
len it = len s &
for i be Nat st i in Seg (len s)
holds it.i = s.(( (i-1+n) mod (len s) ) + 1);
existence
proof
defpred P[Nat,set ] means
$2 = s.(( ($1-1+n) mod (len s) ) + 1);
A2: now let k be Nat;
assume k in Seg (len s);
reconsider i0= (k-1+n) mod (len s) as
Element of NAT by INT_1:3;
A3: 0 + 1 <= i0 + 1 by XREAL_1:6;
i0 + 1 <= (len s) by A1,INT_1:58,NAT_1:13;
then i0 + 1 in dom s by A3,FINSEQ_3:25;
then s.(i0 + 1) in D by FINSEQ_2:11;
hence ex x being Element of D st P[k,x];
end;
consider p being FinSequence of D
such that A4: dom p = Seg (len s) &
for k be Nat st k in Seg (len s) holds P[k,p.k]
from FINSEQ_1:sch 5(A2);
len p = len s by A4,FINSEQ_1:def 3;
hence thesis by A4;
end;
uniqueness
proof
let p,q be FinSequence of D;
assume A5: len p=len s &
for i be Nat
st i in Seg (len s)
holds p.i= s.(( (i-1+n) mod (len s) ) + 1);
assume A6: len q=len s &
for i be Nat st i in Seg (len s)
holds q.i= s.(( (i-1+n) mod (len s) ) + 1);
now let j be Nat;
assume j in dom p;
then
A7:j in Seg (len s) by A5,FINSEQ_1:def 3;
thus p.j = s.(( (j-1+n) mod (len s) ) + 1) by A7,A5
.= q.j by A7,A6;
end;
hence thesis by A5,A6,FINSEQ_2:9;
end;
end;
theorem
for n,m be Integer
st 1 <= len s holds
Op-Shift(Op-Shift(s,n),m)= Op-Shift(s,n+m)
proof
let n,m be Integer;
assume
A1:1 <= len s;
A2:len (Op-Shift(s,n)) = len s &
for i be Nat
st i in Seg (len s)
holds (Op-Shift(s,n)).i = s.(( (i-1+n) mod (len s) ) + 1) by Def3,A1;
A3:len (Op-Shift(s,n+m)) = len s &
for i be Nat
st i in Seg (len s)
holds (Op-Shift(s,n+m)).i
= s.(( (i-1+(n+m)) mod (len s) ) + 1) by Def3,A1;
A4: len (Op-Shift(Op-Shift(s,n),m) )
= len (Op-Shift(s,n+m)) by A3,Def3,A1,A2;
now let i be Nat;
assume A5:i in dom (Op-Shift(Op-Shift(s,n),m) );
then
A6:i in Seg (len s) by A3,A4,FINSEQ_1:def 3;
A7:i in Seg len (Op-Shift(s,n))
by A2,A3,A4,A5,FINSEQ_1:def 3;
reconsider i1= (i-1+m) mod (len s) as
Element of NAT by INT_1:3;
A8: 0 + 1 <= i1 + 1 by XREAL_1:6;
i1 + 1 <= (len s) by A1,INT_1:58,NAT_1:13;
then
A9:i1 + 1 in Seg (len s) by A8;
A10: i1 mod (len s) = (i-1+m) mod (len s) by NAT_D:65;
A11: (i1 + n ) mod (len s)
= ( ( (i-1+m) mod (len s) ) + (n mod (len s)) ) mod (len s)
by A10,NAT_D:66
.=(i-1+m+n) mod (len s) by NAT_D:66;
A12:(Op-Shift(Op-Shift(s,n),m)).i
= (Op-Shift(s,n)).(i1+1) by A7,Def3,A1,A2
.= s.((i1+1 - 1 + n ) mod (len s) + 1) by A9,Def3,A1
.= s.( (i-1+n+m) mod (len s) + 1) by A11;
(Op-Shift(s,n+m)).i = s.(( (i-1+(n+m)) mod (len s) ) + 1)
by A6,Def3,A1;
hence (Op-Shift(Op-Shift(s,n),m) ).i =(Op-Shift(s,n+m)).i by A12;
end;
hence thesis by A4,FINSEQ_2:9;
end;
theorem
1 <= len s implies Op-Shift(s,0)= s
proof
assume A1:1 <= len s;
then
A2:len (Op-Shift(s,0)) = len s &
for i be Nat st i in Seg (len s) holds (Op-Shift(s,0)).i
= s.( (i-1+0) mod (len s) + 1) by Def3;
A3: now let i be Nat;
assume i in dom (Op-Shift(s,0));
then
A4:i in Seg (len s) by A2,FINSEQ_1:def 3;
then
A5: 1<=i & i <=len s by FINSEQ_1:1;
then
A6: 1-1 <= i-1 by XREAL_1:9;
i < len s + 1 by A5,NAT_1:13;
then A7:
i -1 < len s + 1 -1 by XREAL_1:14;
thus (Op-Shift(s,0)).i = s.((i-1+0) mod (len s) + 1) by A4,Def3,A1
.= s.((i-1) + 1) by A7,A6,NAT_D:63
.= s.i;
end;
thus thesis by A2,A3,FINSEQ_2:9;
end;
theorem
1 <= len s implies Op-Shift(s,len s)= s
proof
assume
A1:1 <= len s;
set m = len s;
A2:len Op-Shift(s,m) = m &
for i be Nat st i in Seg m
holds Op-Shift(s,m).i = s.( ( (i-1+ m) mod m ) + 1 ) by Def3,A1;
now let i be Nat;
assume i in dom (Op-Shift(s,m));
then
A3: i in Seg m by A2,FINSEQ_1:def 3;
then
A4: 1<=i & i <=len s by FINSEQ_1:1;
then
A5: 1-1 <= i-1 by XREAL_1:9;
i < len s + 1 by A4,NAT_1:13;
then A6:
i -1 < len s + 1 -1 by XREAL_1:14;
( (i-1+ m) mod m ) + 1
= (((i-1) mod m ) + (m mod m) ) mod m + 1 by NAT_D:66
.= (((i-1) mod m) + 0) mod m + 1 by A1,INT_1:62
.= (i-1) mod m + 1 by NAT_D:65
.= i-1 + 1 by A6,A5,NAT_D:63
.= i;
hence Op-Shift(s,m).i = s.i by A3,Def3,A1;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem
1 <= len s implies Op-Shift(s,-(len s ))= s
proof
assume
A1:1 <= len s;
set m = len s;
A2:len Op-Shift(s,-m) = m &
for i be Nat
st i in Seg m
holds Op-Shift(s,-m).i
= s.( ( (i-1 + - m) mod m ) + 1 ) by Def3,A1;
-m = m*(-1);
then A3:
0 < m & m divides -m by A1,INT_1:def 3;
now let i be Nat;
assume i in dom (Op-Shift(s,-m));
then
A4: i in Seg m by A2,FINSEQ_1:def 3;
then
A5: 1<=i & i <=len s by FINSEQ_1:1;
then
A6: 1-1 <= i-1 by XREAL_1:9;
i < len s + 1 by A5,NAT_1:13;
then A7:
i -1 < len s + 1 -1 by XREAL_1:14;
( (i-1+ -m) mod m ) + 1
= (((i-1) mod m ) + ( (-m) mod m) ) mod m + 1 by NAT_D:66
.= (((i-1) mod m) + 0) mod m + 1 by A3,INT_1:62
.= (i-1) mod m + 1 by NAT_D:65
.= i-1 + 1 by A7,A6,NAT_D:63
.= i;
hence Op-Shift(s,-m).i = s.i
by Def3,A1,A4;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th14:
for n be non zero Element of NAT,
m be Integer,
s be Element of n-tuples_on D
holds Op-Shift(s,m) is Element of n-tuples_on D
proof
let n be non zero Element of NAT,
m be Integer,
s be Element of n-tuples_on D;
A1: len s = n by CARD_1:def 7;
1 <= len s by NAT_1:14;
then len (Op-Shift(s,m)) = len s by Def3;
then Op-Shift(s,m) is Tuple of n,D by A1,CARD_1:def 7;
hence thesis by FINSEQ_2:131;
end;
theorem
1 <= len s implies Op-Shift(s,-1)= Op-RightShift(s)
proof
assume A1: 1 <= len s;
A2:len Op-Shift(s,-1) = len s &
for i be Nat st i in Seg (len s)
holds Op-Shift(s,-1).i = s.( ( (i-1 - 1) mod (len s) ) + 1 )
by Def3,A1;
A3: (Op-RightShift(s)) is FinSequence of D &
len (Op-RightShift(s)) = len s by A1,Th8,Th7;
A4:len <* s.(len s) *> = 1 by FINSEQ_1:40;
now let i be Nat;
assume i in dom (Op-Shift(s,-1));
then
A5: i in Seg (len s) by A2,FINSEQ_1:def 3;
then
A6: 1<=i & i <=len s by FINSEQ_1:1;
i < len s + 1 by A6,NAT_1:13;
then
A7: i -1 < len s + 1 -1 by XREAL_1:14;
now per cases;
suppose A8: i=1;
A9: -1 >= - (len s) by A1,XREAL_1:24;
A10: Op-Shift(s,-1).i
= s.( ((i-1 -1) mod (len s) ) + 1) by A5,Def3,A1
.=s.( (len s) + -1 + 1 ) by A9,A8,NAT_D:63
.=s.(len s);
(Op-RightShift(s)).i
=((<* s.(len s) *>) ^ s ).i by A5,FUNCT_1:49
.= (<* s.(len s) *>).i by A8,A4,FINSEQ_1:64
.= s.(len s) by A8;
hence Op-Shift(s,-1).i = (Op-RightShift(s)).i by A10;
end;
suppose i <> 1;
then A11: 1 < i by A6,XXREAL_0:1;
then
A12:1+1 <= i by NAT_1:13;
i-1-1 <= i-1 by XREAL_1:43;
then A13:
0 <= i-2 & i-2 < len s by A12,A7,XREAL_1:48,XXREAL_0:2;
A14: Op-Shift(s,-1).i
= s.( ( (i-1 -1) mod (len s) ) + 1 ) by A5,Def3,A1
.=s.( i-2 + 1 ) by A13,NAT_D:63
.=s.( i-1);
A15: len (<* s.(len s) *>) + 1 <= i by A11,A4,NAT_1:13;
A16: i <= len (<* s.(len s) *>) + len s by A6,A4,NAT_1:13;
(Op-RightShift(s)).i
=((<* s.(len s) *>) ^ s ).i by A5,FUNCT_1:49
.= s.(i-1) by A15,A16,A4,FINSEQ_1:23;
hence Op-Shift(s,-1).i = (Op-RightShift(s)).i by A14;
end;
end;
hence Op-Shift(s,-1).i = (Op-RightShift(s)).i;
end;
hence thesis by A2,A3,FINSEQ_2:9;
end;
theorem
1 <= len s implies Op-Shift(s,1)= Op-LeftShift(s)
proof
assume A1: 1 <= len s;
A2:len Op-Shift(s,1) = len s &
for i be Nat st i in Seg (len s) holds Op-Shift(s,1).i
= s.( ( (i-1 + 1) mod (len s) ) + 1 ) by Def3,A1;
A3: (Op-LeftShift(s)) is FinSequence of D &
len (Op-LeftShift(s)) = len s by A1,Th5;
A4:len <* s.1 *> = 1 by FINSEQ_1:40;
A5: len (s /^ 1 ) = len s - 1 by A1,RFINSEQ:def 1;
now let i be Nat;
assume i in dom (Op-Shift(s,1));
then
A6: i in Seg (len s) by A2,FINSEQ_1:def 3;
then
A7: 1<=i & i <=len s by FINSEQ_1:1;
now per cases;
suppose A8: i=(len s);
A9: Op-Shift(s,1).i
= s.( ( (i-1 + 1) mod (len s) ) + 1 ) by A6,Def3,A1
.=s.( 0 + 1 ) by A1,A8,INT_1:62
.=s.1;
A10: i <= len ((s /^1)) + len (<* s.1 *>) by A8,A5,A4;
A11: i - len (s /^1) = len s - (len s - 1)
by A8,A1,RFINSEQ:def 1;
(Op-LeftShift(s)).i = (<* s.1 *>).1 by A10,A4,A11,FINSEQ_1:23
.= s.1;
hence Op-Shift(s,1).i = (Op-LeftShift(s)).i by A9;
end;
suppose i <> len s;
then
A12:0 <= i & i < len s by A7,XXREAL_0:1;
i +1 <= len s by A12,NAT_1:13;
then A13:
i + 1 - 1 <= len s -1 by XREAL_1:9;
then
A14: 1 <=i & i <= (len s) -1 by A6,FINSEQ_1:1;
reconsider ls1=len s -1 as Element of NAT by A13,INT_1:3;
i in Seg (ls1) by A14;
then
A15: i in dom (s /^1) by A5,FINSEQ_1:def 3;
A16: Op-Shift(s,1).i
= s.( ( (i-1 + 1) mod (len s) ) + 1 ) by A6,Def3,A1
.=s.( i + 1 ) by A12,NAT_D:63;
(Op-LeftShift(s)).i =(s /^1).i by A5,A14,FINSEQ_1:64
.= s.(i+1) by A15,A1,RFINSEQ:def 1;
hence Op-Shift(s,1).i = (Op-LeftShift(s)).i by A16;
end;
end;
hence Op-Shift(s,1).i = (Op-LeftShift(s)).i;
end;
hence thesis by A2,A3,FINSEQ_2:9;
end;
definition
let x,y be Element of 28-tuples_on BOOLEAN;
redefine func x^y -> Element of 56-tuples_on BOOLEAN; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
len (x^y) = 56 by CARD_1:def 7;
hence thesis by FINSEQ_2:92;
end;
end;
definition
let n be non zero Element of NAT;
let s be Element of n-tuples_on BOOLEAN;
let i be Nat;
redefine func s.i -> Element of BOOLEAN; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose not i in dom s;
then s.i = {} by FUNCT_1:def 2;
hence s.i is Element of BOOLEAN by TARSKI:def 2;
end;
suppose i in dom s;
then s.i in rng s by FUNCT_1:3;
hence s.i is Element of BOOLEAN;
end;
end;
end;
registration
let n be Nat;
cluster -> boolean-valued for Element of n-tuples_on BOOLEAN;
coherence
proof let e be Element of n-tuples_on BOOLEAN;
thus rng e c= BOOLEAN;
end;
end;
notation
let n be Element of NAT;
let s,t be Element of n-tuples_on BOOLEAN;
synonym Op-XOR(s,t) for s 'xor' t;
end;
definition
let n be non zero Element of NAT;
let s,t be Element of n-tuples_on BOOLEAN;
redefine func Op-XOR(s,t) -> Element of n-tuples_on BOOLEAN means :: redefines Op-XOR (DESCIP_1, synonym) → 'xor' (BVFUNC_1, definition)
:Def4:
for i be Nat st i in Seg n holds it.i = s.i 'xor' t.i;
coherence
proof
reconsider s1=s, t1=t as Element of Funcs(Seg n,BOOLEAN) by FINSEQ_2:93;
s1 'xor' t1 is Element of Funcs(Seg n,BOOLEAN) by FUNCT_2:8;
hence thesis by FINSEQ_2:93;
end;
compatibility
proof
let R be Element of n-tuples_on BOOLEAN;
set F = s 'xor' t;
A1: now
let R be Element of n-tuples_on BOOLEAN;
thus dom R = Seg len R by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
end;
then
A2: dom R = Seg n;
hence R = F implies
for i be Nat st i in Seg n holds R.i = s.i 'xor' t.i by BVFUNC_1:def 3;
A3: dom s = Seg n & dom t = Seg n by A1;
A4: Seg n /\ Seg n = Seg n;
assume for i be Nat st i in Seg n holds R.i = s.i 'xor' t.i;
then for x being set st x in dom R holds R.x = (s.x) 'xor' (t.x) by A2;
hence R = F by A1,A3,A4,BVFUNC_1:def 3;
end;
end;
definition
let n,k be non zero Element of NAT,
RK be Element of k-tuples_on (n-tuples_on BOOLEAN);
let i be Element of Seg k;
redefine func RK.i -> Element of n-tuples_on BOOLEAN; :: redefines . (FUNCT_1, definition)
coherence
proof
RK is Element of Funcs(Seg k,n-tuples_on BOOLEAN) by FINSEQ_2:93;
hence RK.i is Element of n-tuples_on BOOLEAN by FUNCT_2:5;
end;
end;
theorem Th17:
for n be non zero Element of NAT,
s,t be Element of n-tuples_on BOOLEAN
holds Op-XOR(Op-XOR(s,t),t) = s
proof
let n be non zero Element of NAT,
s,t be Element of n-tuples_on BOOLEAN;
now let j be Nat;
assume A1: j in Seg n;
thus (Op-XOR(Op-XOR(s,t),t)).j
= (Op-XOR(s,t)).j 'xor' t.j by A1,Def4
.= (s.j 'xor' t.j ) 'xor' t.j by A1,Def4
.= s.j by XBOOLEAN:72;
end;
hence thesis by FINSEQ_2:119;
end;
definition
let m be non zero Element of NAT;
let D be non empty set;
let L be sequence of m-tuples_on D;
let i be Nat;
redefine func L.i -> Element of m-tuples_on D; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
L.i is Element of m-tuples_on D;
hence thesis;
end;
end;
definition
let f be Function of 64,16;
let i be set;
redefine func f.i -> Element of 16; :: redefines . (FUNCT_1, definition)
coherence
proof
f.i in Segm 16
proof
per cases;
suppose i in dom f;
hence thesis by FUNCT_2:5;
end;
suppose not i in dom f;
then f.i=0 by FUNCT_1:def 2;
hence thesis by NAT_1:44;
end;
end;
hence thesis;
end;
end;
theorem Th18:
for n,m be Nat st n+m <= len s holds
(s|n)^((s/^n)|m) = s|(n+m)
proof
let n,m be Nat;
assume A1: n+m <= len s;
set f0=s/^n;
A2:(s|n)^f0 =s by RFINSEQ:8;
set f1=f0|m;
set f2=f0/^m;
set f3=(s|n)^((s/^n)|m);
A3: (s|n)^(f1^f2) =s by A2,RFINSEQ:8;
n <= n+m by NAT_1:11;then
n <= len s by A1,XXREAL_0:2;
then A4: len (s|n)= n &
len f0= len s -n by FINSEQ_1:59,RFINSEQ:def 1;
then n+m <= n + len f0 by A1;
then len f1 = m by FINSEQ_1:59,XREAL_1:6;
then len f3= n+m by A4,FINSEQ_1:22;
then dom f3 = Seg (n+m) by FINSEQ_1:def 3;
hence f3=(f3^f2)|(Seg (n+m)) by FINSEQ_1:21
.=s|(n+m) by A3,FINSEQ_1:32;
end;
scheme
QuadChoiceRec { A, B,C,D() -> non empty set,
A0() -> Element of A(), B0() -> Element of B(),
C0() -> Element of C(), D0() -> Element of D(),
P[object,object,object,object,object,object,object,object,object] }:
ex f being sequence of A(), g being sequence of B(),
h being sequence of C(), i being sequence of D()
st f.0 = A0() & g.0 = B0() &h.0 = C0() & i.0 = D0()
& for n being Element of
NAT holds P[n,f.n,g.n,h.n,i.n,f.(n+1),g.(n+1),h.(n+1),i.(n+1)]
provided
A1: for n being Element of NAT, x being Element of A(), y being Element
of B() , z being Element of C(),w being Element of D()
ex x1 being Element of A(), y1 being Element of B(),
z1 being Element of C(), w1 being Element of D()
st P[n,x,y,z,w,x1,y1,z1,w1]
proof
defpred P1[set,set,set,set,set]
means P[$1,($2)`1,($2)`2,($3)`1,($3)`2,($4)`1,($4)`2,($5)`1,($5)`2];
A2: for n being Nat, x being Element of [:A(),B():],
y being Element of [:C(),D():]
ex z being Element of [:A(),B():],w being Element of [:C(),D():]
st P1[n,x,y,z,w]
proof
let n be Nat, x be Element of [:A(),B():],
y be Element of [:C(),D():];
n in NAT by ORDINAL1:def 12;
then consider ai being Element of A(), bi being Element of B(),
ci being Element of C(), di being Element of D() such that
A3: P[n,x`1,x`2,y`1,y`2,ai,bi,ci,di] by A1;
take z= [ai,bi],w= [ci,di];
thus thesis by A3;
end;
set AB0=[A0(),B0()],CD0=[C0(),D0()];
consider fg being sequence of [:A(),B():],
hi being sequence of [:C(),D():] such that
A4: fg.0 = AB0 and
A5: hi.0 = CD0 and
A6: for e being Nat holds P1[e,fg.e,hi.e,fg.(e+1),hi.(e+1)]
from RECDEF_2:sch 3( A2);
take pr1 fg, pr2 fg,pr1 hi, pr2 hi;
(fg.0)`1 = (pr1 fg).0 & (fg.0)`2 = (pr2 fg).0
& (hi.0)`1 = (pr1 hi).0 & (hi.0)`2 = (pr2 hi).0
by FUNCT_2:def 5,def 6;
hence (pr1 fg).0 = A0() & (pr2 fg).0 = B0()
&(pr1 hi).0 = C0() & (pr2 hi).0 = D0()
by A4,A5;
let i be Element of NAT;
A7: (fg.(i+1))`1 = (pr1 fg).(i+1) & (fg.(i+1))`2 = (pr2 fg).(i+1)
& (hi.(i+1))`1 = (pr1 hi).(i+1) & (hi.(i+1))`2 = (pr2 hi).(i+1)
by FUNCT_2:def 5,def 6;
(fg.i)`1 = (pr1 fg).i & (fg.i)`2 = (pr2 fg).i
& (hi.i)`1 = (pr1 hi).i & (hi.i)`2 = (pr2 hi).i
by FUNCT_2:def 5,def 6;
hence thesis by A6,A7;
end;
theorem
for n be non zero Nat holds n = {0} \/ ((Seg n) \ {n})
proof
let n be non zero Nat;
A1: {0} /\ {n} = {}
proof
assume {0} /\ {n} <> {};
then consider x be object such that
A2: x in {0} /\ {n} by XBOOLE_0:def 1;
x in {0} & x in {n} by A2,XBOOLE_0:def 4;
then x=0 & x= n by TARSKI:def 1;
hence contradiction;
end;
A3: {k where k is Nat: k <= n } = {0}\/ Seg n
proof
now let x be object;
assume x in {k where k is Nat: k <= n };
then
consider m be Nat such that
A4: m=x & m <= n;
m =0 or (1 <= m & m <= n ) by A4,NAT_1:14;
then
m in {0} or m in Seg n by TARSKI:def 1;
hence x in {0}\/ Seg n by A4,XBOOLE_0:def 3;
end;
then
A5:{k where k is Nat: k <= n } c= {0}\/ Seg n by TARSKI:def 3;
now let x be object;
assume A6: x in {0}\/ Seg n;
then reconsider m=x as Element of NAT;
m in {0} or m in Seg n by A6,XBOOLE_0:def 3;
then
m=0 or 1 <= m & m <= n by FINSEQ_1:1,TARSKI:def 1;
hence x in {k where k is Nat: k <= n };
end;
then {0}\/ Seg n c={k where k is Nat: k <= n } by TARSKI:def 3;
hence thesis by A5,XBOOLE_0:def 10;
end;
thus n=succ Segm n \ {n} by ORDINAL1:37
.= {k where k is Nat: k <= n } \ {n} by NAT_1:54
.= ({0} \ {n} ) \/ ((Seg n) \ {n}) by A3,XBOOLE_1:42
.= {0} \/ ((Seg n) \ {n}) by A1,XBOOLE_0:def 7,XBOOLE_1:83;
end;
theorem Th20:
for S be non empty set,
x1,x2,x3,x4,x5,x6,x7,x8 be Element of S holds
ex s be FinSequence of S st
s is 8-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8
proof
let S be non empty set,
x1,x2,x3,x4,x5,x6,x7,x8 be Element of S;
set a1=<*x1,x2,x3,x4*>;
set a2=<*x5,x6,x7,x8*>;
take b1 = a1^a2;
A1: b1.1=a1.1 & ... & b1.4=a1.4 by FINSEQ_3:154;
b1.(4+1)=a2.1 & ... & b1.(4+4)=a2.4 by FINSEQ_3:155;
hence thesis by A1;
end;
theorem Th21:
for S be non empty set,
x1,x2,x3,x4,x5,x6,x7,x8,
x9,x10,x11,x12,x13,x14,x15,x16
be Element of S holds
ex s be FinSequence of S st
s is 16-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8&
s.9=x9&s.10=x10&s.11=x11&s.12=x12&
s.13=x13&s.14=x14&s.15=x15&s.16=x16
proof
let S be non empty set,
x1,x2,x3,x4,x5,x6,x7,x8,
x9,x10,x11,x12,x13,x14,x15,x16 be Element of S;
consider a1 be FinSequence of S such that
A1: a1 is 8-element &
a1.1=x1&a1.2=x2&a1.3=x3&a1.4=x4&
a1.5=x5&a1.6=x6&a1.7=x7&a1.8=x8 by Th20;
consider a2 be FinSequence of S such that
A2: a2 is 8-element &
a2.1=x9&a2.2=x10&a2.3=x11&a2.4=x12&
a2.5=x13&a2.6=x14&a2.7=x15&a2.8=x16 by Th20;
reconsider a1,a2 as 8-element FinSequence of S by A1,A2;
take a1^a2;
thus a1^a2 is 16-element;
A3: (a1^a2).1 = a1.1 & ... & (a1^a2).8 = a1.8 by FINSEQ_3:154;
(a1^a2).(8+1) = a2.1 & ... & (a1^a2).(8+8) = a2.8
by FINSEQ_3:155;
hence thesis by A3,A1,A2;
end;
theorem Th22:
for S be non empty set,
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
be Element of S holds
ex s be FinSequence of S st
s is 32-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8&
s.9=x9&s.10=x10&s.11=x11&s.12=x12&
s.13=x13&s.14=x14&s.15=x15&s.16=x16 &
s.17=x17&s.18=x18&s.19=x19&s.20=x20&
s.21=x21&s.22=x22&s.23=x23&s.24=x24&
s.25=x25&s.26=x26&s.27=x27&s.28=x28&
s.29=x29&s.30=x30&s.31=x31&s.32=x32
proof
let S be non empty set,
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 be Element of S;
consider a1 be FinSequence of S such that
A1:a1 is 16-element &
a1.1=x1&a1.2=x2&a1.3=x3&a1.4=x4&
a1.5=x5&a1.6=x6&a1.7=x7&a1.8=x8&
a1.9=x9&a1.10=x10&a1.11=x11&a1.12=x12&
a1.13=x13&a1.14=x14&a1.15=x15&a1.16=x16 by Th21;
consider a2 be FinSequence of S such that
A2:a2 is 16-element &
a2.1=x17&a2.2=x18&a2.3=x19&a2.4=x20&
a2.5=x21&a2.6=x22&a2.7=x23&a2.8=x24&
a2.9=x25&a2.10=x26&a2.11=x27&a2.12=x28&
a2.13=x29&a2.14=x30&a2.15=x31&a2.16=x32 by Th21;
reconsider a1,a2 as 16-element FinSequence of S by A1,A2;
take a1^a2;
thus a1^a2 is 32-element;
A3: (a1^a2).1 = a1.1 & ... & (a1^a2).16 = a1.16 by FINSEQ_3:154;
(a1^a2).(16+1) = a2.1 & ... & (a1^a2).(16+16) = a2.16
by FINSEQ_3:155;
hence thesis by A3,A1,A2;
end;
theorem Th23:
for S be non empty set,
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
be Element of S holds
ex s be FinSequence of S st
s is 48-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8&
s.9=x9&s.10=x10&s.11=x11&s.12=x12&
s.13=x13&s.14=x14&s.15=x15&s.16=x16 &
s.17=x17&s.18=x18&s.19=x19&s.20=x20&
s.21=x21&s.22=x22&s.23=x23&s.24=x24&
s.25=x25&s.26=x26&s.27=x27&s.28=x28&
s.29=x29&s.30=x30&s.31=x31&s.32=x32&
s.33=x33&s.34=x34&s.35=x35&s.36=x36&
s.37=x37&s.38=x38&s.39=x39&s.40=x40&
s.41=x41&s.42=x42&s.43=x43&s.44=x44&
s.45=x45&s.46=x46&s.47=x47&s.48=x48
proof
let S be non empty set,
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 be Element of S;
consider a1 be FinSequence of S such that
A1:a1 is 32-element &
a1.1=x1&a1.2=x2&a1.3=x3&a1.4=x4&
a1.5=x5&a1.6=x6&a1.7=x7&a1.8=x8&
a1.9=x9&a1.10=x10&a1.11=x11&a1.12=x12&
a1.13=x13&a1.14=x14&a1.15=x15&a1.16=x16 &
a1.17=x17&a1.18=x18&a1.19=x19&a1.20=x20&
a1.21=x21&a1.22=x22&a1.23=x23&a1.24=x24&
a1.25=x25&a1.26=x26&a1.27=x27&a1.28=x28&
a1.29=x29&a1.30=x30&a1.31=x31&a1.32=x32
by Th22;
consider a2 be FinSequence of S such that
A2:a2 is 16-element &
a2.1=x33&a2.2=x34&a2.3=x35&a2.4=x36&
a2.5=x37&a2.6=x38&a2.7=x39&a2.8=x40&
a2.9=x41&a2.10=x42&a2.11=x43&a2.12=x44&
a2.13=x45&a2.14=x46&a2.15=x47&a2.16=x48 by Th21;
reconsider a1 as 32-element FinSequence of S by A1;
reconsider a2 as 16-element FinSequence of S by A2;
take a1^a2;
thus a1^a2 is 48-element;
A3: (a1^a2).1 = a1.1 & ... & (a1^a2).32 = a1.32 by FINSEQ_3:154;
(a1^a2).(32+1) = a2.1 & ... & (a1^a2).(32+16) = a2.16
by FINSEQ_3:155;
hence thesis by A3,A1,A2;
end;
theorem Th24:
for S be non empty set,
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 be Element of S holds
ex s be FinSequence of S st
s is 56-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8&
s.9=x9&s.10=x10&s.11=x11&s.12=x12&
s.13=x13&s.14=x14&s.15=x15&s.16=x16 &
s.17=x17&s.18=x18&s.19=x19&s.20=x20&
s.21=x21&s.22=x22&s.23=x23&s.24=x24&
s.25=x25&s.26=x26&s.27=x27&s.28=x28&
s.29=x29&s.30=x30&s.31=x31&s.32=x32&
s.33=x33&s.34=x34&s.35=x35&s.36=x36&
s.37=x37&s.38=x38&s.39=x39&s.40=x40&
s.41=x41&s.42=x42&s.43=x43&s.44=x44&
s.45=x45&s.46=x46&s.47=x47&s.48=x48&
s.49=x49&s.50=x50&s.51=x51&s.52=x52&
s.53=x53&s.54=x54&s.55=x55&s.56=x56
proof
let S be non empty set,
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 be Element of S;
consider a1 be FinSequence of S such that
A1:a1 is 48-element &
a1.1=x1&a1.2=x2&a1.3=x3&a1.4=x4&
a1.5=x5&a1.6=x6&a1.7=x7&a1.8=x8&
a1.9=x9&a1.10=x10&a1.11=x11&a1.12=x12&
a1.13=x13&a1.14=x14&a1.15=x15&a1.16=x16 &
a1.17=x17&a1.18=x18&a1.19=x19&a1.20=x20&
a1.21=x21&a1.22=x22&a1.23=x23&a1.24=x24&
a1.25=x25&a1.26=x26&a1.27=x27&a1.28=x28&
a1.29=x29&a1.30=x30&a1.31=x31&a1.32=x32&
a1.33=x33&a1.34=x34&a1.35=x35&a1.36=x36&
a1.37=x37&a1.38=x38&a1.39=x39&a1.40=x40&
a1.41=x41&a1.42=x42& a1.43=x43&a1.44=x44&
a1.45=x45&a1.46=x46&a1.47=x47&a1.48=x48 by Th23;
consider a2 be FinSequence of S such that
A2:a2 is 8-element &
a2.1=x49&a2.2=x50&a2.3=x51&a2.4=x52&
a2.5=x53&a2.6=x54&a2.7=x55&a2.8=x56 by Th20;
reconsider a1 as 48-element FinSequence of S by A1;
reconsider a2 as 8-element FinSequence of S by A2;
take a1^a2;
thus a1^a2 is 56-element;
A3: (a1^a2).1 = a1.1 & ... & (a1^a2).48 = a1.48 by FINSEQ_3:154;
(a1^a2).(48+1) = a2.1 & ... & (a1^a2).(48+8) = a2.8
by FINSEQ_3:155;
hence thesis by A3,A1,A2;
end;
theorem Th25:
for S be non empty set,
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 be Element of S holds
ex s be FinSequence of S st
s is 64-element &
s.1=x1&s.2=x2&s.3=x3&s.4=x4&
s.5=x5&s.6=x6&s.7=x7&s.8=x8&
s.9=x9&s.10=x10&s.11=x11&s.12=x12&
s.13=x13&s.14=x14&s.15=x15&s.16=x16 &
s.17=x17&s.18=x18&s.19=x19&s.20=x20&
s.21=x21&s.22=x22&s.23=x23&s.24=x24&
s.25=x25&s.26=x26&s.27=x27&s.28=x28&
s.29=x29&s.30=x30&s.31=x31&s.32=x32&
s.33=x33&s.34=x34&s.35=x35&s.36=x36&
s.37=x37&s.38=x38&s.39=x39&s.40=x40&
s.41=x41&s.42=x42&s.43=x43&s.44=x44&
s.45=x45&s.46=x46&s.47=x47&s.48=x48&
s.49=x49&s.50=x50&s.51=x51&s.52=x52&
s.53=x53&s.54=x54&s.55=x55&s.56=x56&
s.57=x57&s.58=x58&s.59=x59&s.60=x60&
s.61=x61&s.62=x62&s.63=x63&s.64=x64
proof
let S be non empty set,
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 be Element of S;
consider a1 be FinSequence of S such that
A1:a1 is 32-element &
a1.1=x1&a1.2=x2&a1.3=x3&a1.4=x4&
a1.5=x5&a1.6=x6&a1.7=x7&a1.8=x8&
a1.9=x9&a1.10=x10&a1.11=x11&a1.12=x12&
a1.13=x13&a1.14=x14&a1.15=x15&a1.16=x16 &
a1.17=x17&a1.18=x18&a1.19=x19&a1.20=x20&
a1.21=x21&a1.22=x22&a1.23=x23&a1.24=x24&
a1.25=x25&a1.26=x26&a1.27=x27&a1.28=x28&
a1.29=x29&a1.30=x30&a1.31=x31&a1.32=x32 by Th22;
consider a2 be FinSequence of S such that
A2:a2 is 32-element &
a2.1=x33&a2.2=x34&a2.3=x35&a2.4=x36&
a2.5=x37&a2.6=x38&a2.7=x39&a2.8=x40&
a2.9=x41&a2.10=x42&a2.11=x43&a2.12=x44&
a2.13=x45&a2.14=x46&a2.15=x47&a2.16=x48&
a2.17=x49&a2.18=x50&a2.19=x51&a2.20=x52&
a2.21=x53&a2.22=x54&a2.23=x55&a2.24=x56&
a2.25=x57&a2.26=x58&a2.27=x59&a2.28=x60&
a2.29=x61&a2.30=x62&a2.31=x63&a2.32=x64 by Th22;
reconsider a1,a2 as 32-element FinSequence of S by A1,A2;
take a1^a2;
thus a1^a2 is 64-element;
A3: (a1^a2).1 = a1.1 & ... & (a1^a2).32 = a1.32 by FINSEQ_3:154;
(a1^a2).(32+1) = a2.1 & ... & (a1^a2).(32+32) = a2.32
by FINSEQ_3:155;
hence thesis by A3,A1,A2;
end;
notation
let n be non zero Nat, i be Element of Segm n;
synonym ntoSeg(i) for succ i;
end;
definition
let n be non zero Nat,
i be Element of Segm n;
redefine func ntoSeg(i) -> Element of Seg n; :: redefines ntoSeg (DESCIP_1, synonym) → succ (ORDINAL1, definition)
coherence
proof
succ Segm i = Segm(i+1) by NAT_1:38;
hence thesis by FINSEQ_3:11,NAT_1:44;
end;
end;
definition
let n be non zero Nat,
f be Function of Segm n, Seg n;
attr f is NtoSEG means
:Def5:
for i be Element of Segm n holds f.i=ntoSeg(i);
end;
registration
let n be non zero Nat;
cluster NtoSEG for Function of Segm n, Seg n;
existence
proof
deffunc F(Element of Segm n) = ntoSeg($1);
A1: for x being Element of Segm n holds F(x) is Element of Seg n;
consider f being Function of Segm n, Seg n such that
A2: for x being Element of Segm n holds f.x = F(x)
from FUNCT_2:sch 9(A1);
take f;
thus thesis by A2;
end;
end;
Lm1:
for n be non zero Nat, f be NtoSEG Function of Segm n, Seg n holds
rng f = Seg n
proof
let n be non zero Nat,
f be NtoSEG Function of Segm n, Seg n;
A1: dom f =n by FUNCT_2:def 1;
now let x be object;assume x in Seg n;
then
consider xk be Nat such that
A2: x=xk & 1 <= xk & xk <= n;
xk-1 is Element of NAT& xk-1 < n by A2,NAT_1:21,XREAL_1:147;
then reconsider i=xk-1 as Element of Segm n by NAT_1:44;
f.i = ntoSeg i by Def5
.= succ Segm i
.= Segm(i+1) by NAT_1:38;
hence x in rng f by A1,A2,FUNCT_1:def 3;
end;
then Seg n c= rng f by TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
registration
let n be non zero Nat;
cluster -> bijective for NtoSEG Function of Segm n, Seg n;
coherence
proof
let f be NtoSEG Function of Segm n, Seg n;
thus f is one-to-one
proof
let x1,x2 be object;
assume A1:x1 in dom f & x2 in dom f & f.x1 = f.x2;
reconsider x1,x2 as Element of Segm n by A1;
Segm(x1+1) = succ Segm x1 by NAT_1:38
.= ntoSeg x1
.= f.x2 by A1,Def5
.= ntoSeg x2 by Def5
.= succ Segm x2
.= Segm(x2+1) by NAT_1:38;
hence thesis;
end;
thus rng f = Seg n by Lm1;
end;
end;
theorem Th26:
for n be non zero Nat,
f be NtoSEG Function of Segm n, Seg n,
i be Nat st i < n holds f.i=i+1 & i in dom f
proof
let n be non zero Nat,
f be NtoSEG Function of Segm n, Seg n,
i be Nat;
assume i < n;then
A1:i in Segm n by NAT_1:44;then
consider ii be Element of Segm n such that A2:ii=i;
A3: ntoSeg ii = succ Segm ii
.=Segm(ii+1) by NAT_1:38;
thus f.i = i+1 by Def5,A2,A3;
thus i in dom f by A1,FUNCT_2:def 1;
end;
Lm2:
for f be NtoSEG Function of Segm 64, Seg 64,
S be non empty set,
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 be Element of S,
t be Element of 64-tuples_on S st
t.1=x1&t.2=x2&t.3=x3&t.4=x4&t.5=x5&t.6=x6&
t.7=x7&t.8=x8&t.9=x9&t.10=x10&t.11=x11&t.12=x12&
t.13=x13&t.14=x14&t.15=x15&t.16=x16&t.17=x17&t.18=x18&
t.19=x19&t.20=x20&t.21=x21&t.22=x22&t.23=x23&t.24=x24&
t.25=x25&t.26=x26&t.27=x27&t.28=x28&t.29=x29&t.30=x30&
t.31=x31&t.32=x32&t.33=x33&t.34=x34&t.35=x35&t.36=x36&
t.37=x37&t.38=x38&t.39=x39&t.40=x40&t.41=x41&t.42=x42&
t.43=x43&t.44=x44&t.45=x45&t.46=x46&t.47=x47&t.48=x48&
t.49=x49&t.50=x50&t.51=x51&t.52=x52&t.53=x53&t.54=x54&
t.55=x55&t.56=x56&t.57=x57&t.58=x58&t.59=x59&t.60=x60&
t.61=x61&t.62=x62&t.63=x63&t.64=x64
holds
(t*f).0=x1&(t*f).1=x2&(t*f).2=x3&(t*f).3=x4&
(t*f).4=x5&(t*f).5=x6&(t*f).6=x7&(t*f).7=x8&
(t*f).8=x9&(t*f).9=x10&(t*f).10=x11&(t*f).11=x12&
(t*f).12=x13&(t*f).13=x14&(t*f).14=x15&(t*f).15=x16&
(t*f).16=x17&(t*f).17=x18&(t*f).18=x19&(t*f).19=x20&
(t*f).20=x21&(t*f).21=x22&(t*f).22=x23&(t*f).23=x24&
(t*f).24=x25&(t*f).25=x26&(t*f).26=x27&(t*f).27=x28&
(t*f).28=x29&(t*f).29=x30&(t*f).30=x31&(t*f).31=x32&
(t*f).32=x33&(t*f).33=x34&(t*f).34=x35&(t*f).35=x36&
(t*f).36=x37&(t*f).37=x38&(t*f).38=x39&(t*f).39=x40&
(t*f).40=x41&(t*f).41=x42&(t*f).42=x43&(t*f).43=x44&
(t*f).44=x45&(t*f).45=x46&(t*f).46=x47&(t*f).47=x48&
(t*f).48=x49&(t*f).49=x50&(t*f).50=x51&(t*f).51=x52&
(t*f).52=x53&(t*f).53=x54&(t*f).54=x55&(t*f).55=x56&
(t*f).56=x57&(t*f).57=x58&(t*f).58=x59&(t*f).59=x60&
(t*f).60=x61&(t*f).61=x62&(t*f).62=x63&(t*f).63=x64
proof
let f be NtoSEG Function of Segm 64, Seg 64,
S be non empty set,
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 be Element of S,
t be Element of 64-tuples_on S;
assume 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;
then
t.(0+1)=x1&t.(1+1)=x2&t.(2+1)=x3&t.(3+1)=x4&
t.(4+1)=x5&t.(5+1)=x6&t.(6+1)=x7&t.(7+1)=x8&
t.(8+1)=x9&t.(9+1)=x10&t.(10+1)=x11&t.(11+1)=x12&
t.(12+1)=x13&t.(13+1)=x14&t.(14+1)=x15&t.(15+1)=x16&
t.(16+1)=x17&t.(17+1)=x18&t.(18+1)=x19&t.(19+1)=x20&
t.(20+1)=x21&t.(21+1)=x22&t.(22+1)=x23&t.(23+1)=x24&
t.(24+1)=x25&t.(25+1)=x26&t.(26+1)=x27&t.(27+1)=x28&
t.(28+1)=x29&t.(29+1)=x30&t.(30+1)=x31&t.(31+1)=x32&
t.(32+1)=x33&t.(33+1)=x34&t.(34+1)=x35&t.(35+1)=x36&
t.(36+1)=x37&t.(37+1)=x38&t.(38+1)=x39&t.(39+1)=x40&
t.(40+1)=x41&t.(41+1)=x42&t.(42+1)=x43&t.(43+1)=x44&
t.(44+1)=x45&t.(45+1)=x46&t.(46+1)=x47&t.(47+1)=x48&
t.(48+1)=x49&t.(49+1)=x50&t.(50+1)=x51&t.(51+1)=x52&
t.(52+1)=x53&t.(53+1)=x54&t.(54+1)=x55&t.(55+1)=x56&
t.(56+1)=x57&t.(57+1)=x58&t.(58+1)=x59&t.(59+1)=x60&
t.(60+1)=x61&t.(61+1)=x62&t.(62+1)=x63&t.(63+1)=x64;
then A1:
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 by Th26;
0 in dom f & ... & 63 in dom f by Th26;
hence thesis by A1,FUNCT_1:13;
end;
theorem Th27:
for S be non empty set,
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 be Element of S holds
ex f be Function of 64, S st
f.0=x1&f.1=x2&f.2=x3&f.3=x4&
f.4=x5&f.5=x6&f.6=x7&f.7=x8&
f.8=x9&f.9=x10&f.10=x11&f.11=x12&
f.12=x13&f.13=x14&f.14=x15&f.15=x16&
f.16=x17&f.17=x18&f.18=x19&f.19=x20&
f.20=x21&f.21=x22&f.22=x23&f.23=x24&
f.24=x25&f.25=x26&f.26=x27&f.27=x28&
f.28=x29&f.29=x30&f.30=x31&f.31=x32&
f.32=x33&f.33=x34&f.34=x35&f.35=x36&
f.36=x37&f.37=x38&f.38=x39&f.39=x40&
f.40=x41&f.41=x42&f.42=x43&f.43=x44&
f.44=x45&f.45=x46&f.46=x47&f.47=x48&
f.48=x49&f.49=x50&f.50=x51&f.51=x52&
f.52=x53&f.53=x54&f.54=x55&f.55=x56&
f.56=x57&f.57=x58&f.58=x59&f.59=x60&
f.60=x61&f.61=x62&f.62=x63&f.63=x64
proof
let S be non empty set,
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 be Element of S;
consider t be FinSequence of S such that
A1: t is 64-element &
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 by Th25;
A2:len t =64 by A1;
set f = the NtoSEG Function of Segm 64, Seg 64;
rng f =Seg 64 by FUNCT_2:def 3;
then
f"(dom t)=f"(rng f) by A2,FINSEQ_1:def 3
.= dom f by RELAT_1:134;then
A3:dom (t*f)=dom f by RELAT_1:147
.= 64 by FUNCT_2:def 1;
A4:rng(t*f) c= S;
reconsider t as Element of 64-tuples_on S by A2,FINSEQ_2:92;
reconsider tf= t*f as Function of 64,S by A3,A4,FUNCT_2:2;
take tf;
thus thesis by A1,Lm2;
end;
Lm3:
0 is Element of Segm 16 & ... & 15 is Element of Segm 16 by NAT_1:44;
Lm4:
for x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,
x11,x12,x13,x14,x15,x16,
x17,x18,x19,x20,x21,x22,x23,x24,
x25,x26,x27,x28,x29,x30,x31,x32,
x33,x34,x35,x36,x37,x38,x39,x40,
x41,x42,x43,x44,x45,x46,x47,x48,
x49,x50,x51,x52,x53,x54,x55,x56,
x57,x58,x59,x60,x61,x62,x63,x64
be Element of 16, f,g be Function of 64,16 st
f.1=x1&f.2=x2&f.3=x3&f.4=x4&
f.5=x5&f.6=x6&f.7=x7&f.8=x8&
f.9=x9&f.10=x10&f.11=x11&f.12=x12&
f.13=x13&f.14=x14&f.15=x15&f.16=x16 &
f.17=x17&f.18=x18&f.19=x19&f.20=x20&
f.21=x21&f.22=x22&f.23=x23&f.24=x24&
f.25=x25&f.26=x26&f.27=x27&f.28=x28&
f.29=x29&f.30=x30&f.31=x31&f.32=x32&
f.33=x33&f.34=x34&f.35=x35&f.36=x36&
f.37=x37&f.38=x38&f.39=x39&f.40=x40&
f.41=x41&f.42=x42&f.43=x43&f.44=x44&
f.45=x45&f.46=x46&f.47=x47&f.48=x48&
f.49=x49&f.50=x50&f.51=x51&f.52=x52&
f.53=x53&f.54=x54&f.55=x55&f.56=x56&
f.57=x57&f.58=x58&f.59=x59&f.60=x60&
f.61=x61&f.62=x62&f.63=x63&f.0=x64&
g.1=x1&g.2=x2&g.3=x3&g.4=x4&
g.5=x5&g.6=x6&g.7=x7&g.8=x8&
g.9=x9&g.10=x10&g.11=x11&g.12=x12&
g.13=x13&g.14=x14&g.15=x15&g.16=x16 &
g.17=x17&g.18=x18&g.19=x19&g.20=x20&
g.21=x21&g.22=x22&g.23=x23&g.24=x24&
g.25=x25&g.26=x26&g.27=x27&g.28=x28&
g.29=x29&g.30=x30&g.31=x31&g.32=x32&
g.33=x33&g.34=x34&g.35=x35&g.36=x36&
g.37=x37&g.38=x38&g.39=x39&g.40=x40&
g.41=x41&g.42=x42&g.43=x43&g.44=x44&
g.45=x45&g.46=x46&g.47=x47&g.48=x48&
g.49=x49&g.50=x50&g.51=x51&g.52=x52&
g.53=x53&g.54=x54&g.55=x55&g.56=x56&
g.57=x57&g.58=x58&g.59=x59&g.60=x60&
g.61=x61&g.62=x62&g.63=x63&g.0=x64
holds
f=g
proof
let 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
be Element of 16, f,g be Function of 64,16;
assume A1:
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;
A2: dom f =63+1 & dom g =64 by FUNCT_2:def 1;
for i be object st i in dom f holds f.i = g.i
proof
let i be object;
assume i in dom f;
then i in Segm(63+1);
then i=0 or ... or i=63 by NAT_1:61;
hence thesis by A1;
end;
hence thesis by A2;
end;
begin :: S-Boxes
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
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 by Th27,Lm3;
uniqueness by Lm4;
end;
begin :: Initial Permutation
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 64-element &
e.1=r.58 & e.2=r.50 & e.3=r.42 & e.4=r.34 & e.5=r.26 &
e.6=r.18 & e.7=r.10 & e.8=r.2 & e.9=r.60 & e.10=r.52 &
e.11=r.44 & e.12=r.36 & e.13=r.28 & e.14=r.20 & e.15=r.12 &
e.16=r.4 & e.17=r.62 & e.18=r.54 & e.19=r.46 & e.20=r.38 &
e.21=r.30 & e.22=r.22 & e.23=r.14 & e.24=r.6 & e.25=r.64 &
e.26=r.56 & e.27=r.48 & e.28=r.40 & e.29=r.32 & e.30=r.24 &
e.31=r.16 & e.32=r.8 & e.33=r.57 & e.34=r.49 & e.35=r.41 &
e.36=r.33 & e.37=r.25 & e.38=r.17 & e.39=r.9 & e.40=r.1 &
e.41=r.59 & e.42=r.51 & e.43=r.43 & e.44=r.35 & e.45=r.27 &
e.46=r.19 & e.47=r.11 & e.48=r.3 & e.49=r.61 & e.50=r.53 &
e.51=r.45 & e.52=r.37 & e.53=r.29 & e.54=r.21 & e.55=r.13 &
e.56=r.5 & e.57=r.63 & e.58=r.55 & e.59=r.47 & e.60=r.39 &
e.61=r.31 & e.62=r.23 & e.63=r.15 & e.64=r.7 by Th25;
len e =64 by A1;then
reconsider e as Element of 64-tuples_on BOOLEAN
by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 64-tuples_on BOOLEAN;
assume A2:
p.1=r.58 & p.2=r.50 & p.3=r.42 & p.4=r.34 & p.5=r.26 &
p.6=r.18 & p.7=r.10 & p.8=r.2 & p.9=r.60 & p.10=r.52 &
p.11=r.44 & p.12=r.36 & p.13=r.28 & p.14=r.20 & p.15=r.12 &
p.16=r.4 & p.17=r.62 & p.18=r.54 & p.19=r.46 & p.20=r.38 &
p.21=r.30 & p.22=r.22 & p.23=r.14 & p.24=r.6 & p.25=r.64 &
p.26=r.56 & p.27=r.48 & p.28=r.40 & p.29=r.32 & p.30=r.24 &
p.31=r.16 & p.32=r.8 & p.33=r.57 & p.34=r.49 & p.35=r.41 &
p.36=r.33 & p.37=r.25 & p.38=r.17 & p.39=r.9 & p.40=r.1 &
p.41=r.59 & p.42=r.51 & p.43=r.43 & p.44=r.35 & p.45=r.27 &
p.46=r.19 & p.47=r.11 & p.48=r.3 & p.49=r.61 & p.50=r.53 &
p.51=r.45 & p.52=r.37 & p.53=r.29 & p.54=r.21 & p.55=r.13 &
p.56=r.5 & p.57=r.63 & p.58=r.55 & p.59=r.47 & p.60=r.39 &
p.61=r.31 & p.62=r.23 & p.63=r.15 & p.64=r.7;
assume A3:
q.1=r.58 & q.2=r.50 & q.3=r.42 & q.4=r.34 & q.5=r.26 &
q.6=r.18 & q.7=r.10 & q.8=r.2 & q.9=r.60 & q.10=r.52 &
q.11=r.44 & q.12=r.36 & q.13=r.28 & q.14=r.20 & q.15=r.12 &
q.16=r.4 & q.17=r.62 & q.18=r.54 & q.19=r.46 & q.20=r.38 &
q.21=r.30 & q.22=r.22 & q.23=r.14 & q.24=r.6 & q.25=r.64 &
q.26=r.56 & q.27=r.48 & q.28=r.40 & q.29=r.32 & q.30=r.24 &
q.31=r.16 & q.32=r.8 & q.33=r.57 & q.34=r.49 & q.35=r.41 &
q.36=r.33 & q.37=r.25 & q.38=r.17 & q.39=r.9 & q.40=r.1 &
q.41=r.59 & q.42=r.51 & q.43=r.43 & q.44=r.35 & q.45=r.27 &
q.46=r.19 & q.47=r.11 & q.48=r.3 & q.49=r.61 & q.50=r.53 &
q.51=r.45 & q.52=r.37 & q.53=r.29 & q.54=r.21 & q.55=r.13 &
q.56=r.5 & q.57=r.63 & q.58=r.55 & q.59=r.47 & q.60=r.39 &
q.61=r.31 & q.62=r.23 & q.63=r.15 & q.64=r.7;
p in { s where s is Element of BOOLEAN*: len s = 64 };
then consider t be Element of BOOLEAN* such that
A4: p = t & len t = 64;
q in { s where s is Element of BOOLEAN*: len s = 64 };
then consider s be Element of BOOLEAN* such that
A5: q = s & len s = 64;
A6: dom p = Seg 64 & dom q =Seg 64 by A4,A5,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p; then
i=1 or ... or i=64 by A6,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A6;
end;
end;
definition
func DES-PIP ->
Function of 64-tuples_on BOOLEAN,64-tuples_on BOOLEAN
means :Def15:
for i be Element of 64-tuples_on BOOLEAN holds it.i = DES-IP(i);
existence
proof
deffunc F(Element of 64-tuples_on BOOLEAN) = DES-IP($1);
A1: for x being Element of 64-tuples_on BOOLEAN holds
F(x) is Element of 64-tuples_on BOOLEAN;
consider f being
Function of 64-tuples_on BOOLEAN, 64-tuples_on BOOLEAN such that
A2: for x being Element of 64-tuples_on BOOLEAN holds f.x = F(x)
from FUNCT_2:sch 9(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of 64-tuples_on BOOLEAN,64-tuples_on BOOLEAN;
assume A3:
for i be Element of 64-tuples_on BOOLEAN holds
f.i= DES-IP(i);
assume A4:
for i be Element of 64-tuples_on BOOLEAN holds
g.i= DES-IP(i);
for i be object st i in 64-tuples_on BOOLEAN
holds f.i=g.i
proof
let i be object;
assume i in 64-tuples_on BOOLEAN;
then
reconsider i as Element of 64-tuples_on BOOLEAN;
f.i=DES-IP(i) by A3
.=g.i by A4;
hence thesis;
end;
hence thesis;
end;
end;
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 64-element &
e.1=r.40 & e.2=r.8 & e.3=r.48 & e.4=r.16 &
e.5=r.56 &e.6=r.24 & e.7=r.64 & e.8=r.32 &
e.9=r.39 & e.10=r.7 &e.11=r.47 & e.12=r.15 &
e.13=r.55 & e.14=r.23 & e.15=r.63 &e.16=r.31 &
e.17=r.38 & e.18=r.6 & e.19=r.46 & e.20=r.14 &
e.21=r.54 & e.22=r.22 & e.23=r.62 & e.24=r.30 &
e.25=r.37 &e.26=r.5 & e.27=r.45 & e.28=r.13 &
e.29=r.53 & e.30=r.21 &e.31=r.61 & e.32=r.29 &
e.33=r.36 & e.34=r.4 & e.35=r.44 &e.36=r.12 &
e.37=r.52 & e.38=r.20 & e.39=r.60 & e.40=r.28 &
e.41=r.35 & e.42=r.3 & e.43=r.43 & e.44=r.11 &
e.45=r.51 &e.46=r.19 & e.47=r.59 & e.48=r.27 &
e.49=r.34 & e.50=r.2 &e.51=r.42 & e.52=r.10 &
e.53=r.50 & e.54=r.18 & e.55=r.58 &e.56=r.26 &
e.57=r.33 & e.58=r.1 & e.59=r.41 & e.60=r.9 &
e.61=r.49 & e.62=r.17 & e.63=r.57 & e.64=r.25 by Th25;
len e =64 by A1;then
reconsider e as Element of 64-tuples_on BOOLEAN by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 64-tuples_on BOOLEAN;
assume A2:
p.1=r.40 & p.2=r.8 & p.3=r.48 & p.4=r.16 &
p.5=r.56 &p.6=r.24 & p.7=r.64 & p.8=r.32 &
p.9=r.39 & p.10=r.7 &p.11=r.47 & p.12=r.15 &
p.13=r.55 & p.14=r.23 & p.15=r.63 &p.16=r.31 &
p.17=r.38 & p.18=r.6 & p.19=r.46 & p.20=r.14 &
p.21=r.54 & p.22=r.22 & p.23=r.62 & p.24=r.30 &
p.25=r.37 &p.26=r.5 & p.27=r.45 & p.28=r.13 &
p.29=r.53 & p.30=r.21 &p.31=r.61 & p.32=r.29 &
p.33=r.36 & p.34=r.4 & p.35=r.44 &p.36=r.12 &
p.37=r.52 & p.38=r.20 & p.39=r.60 & p.40=r.28 &
p.41=r.35 & p.42=r.3 & p.43=r.43 & p.44=r.11 &
p.45=r.51 &p.46=r.19 & p.47=r.59 & p.48=r.27 &
p.49=r.34 & p.50=r.2 &p.51=r.42 & p.52=r.10 &
p.53=r.50 & p.54=r.18 & p.55=r.58 &p.56=r.26 &
p.57=r.33 & p.58=r.1 & p.59=r.41 & p.60=r.9 &
p.61=r.49 & p.62=r.17 & p.63=r.57 & p.64=r.25;
assume A3:
q.1=r.40 & q.2=r.8 & q.3=r.48 & q.4=r.16 &
q.5=r.56 &q.6=r.24 & q.7=r.64 & q.8=r.32 &
q.9=r.39 & q.10=r.7 &q.11=r.47 & q.12=r.15 &
q.13=r.55 & q.14=r.23 & q.15=r.63 &q.16=r.31 &
q.17=r.38 & q.18=r.6 & q.19=r.46 & q.20=r.14 &
q.21=r.54 & q.22=r.22 & q.23=r.62 & q.24=r.30 &
q.25=r.37 &q.26=r.5 & q.27=r.45 & q.28=r.13 &
q.29=r.53 & q.30=r.21 &q.31=r.61 & q.32=r.29 &
q.33=r.36 & q.34=r.4 & q.35=r.44 &q.36=r.12 &
q.37=r.52 & q.38=r.20 & q.39=r.60 & q.40=r.28 &
q.41=r.35 & q.42=r.3 & q.43=r.43 & q.44=r.11 &
q.45=r.51 &q.46=r.19 & q.47=r.59 & q.48=r.27 &
q.49=r.34 & q.50=r.2 &q.51=r.42 & q.52=r.10 &
q.53=r.50 & q.54=r.18 & q.55=r.58 &q.56=r.26 &
q.57=r.33 & q.58=r.1 & q.59=r.41 & q.60=r.9 &
q.61=r.49 & q.62=r.17 & q.63=r.57 & q.64=r.25;
p in { s where s is Element of BOOLEAN*: len s = 64 };
then consider t be Element of BOOLEAN* such that
A4: p = t & len t = 64;
q in { s where s is Element of BOOLEAN*: len s = 64 };
then consider s be Element of BOOLEAN* such that
A5: q = s & len s = 64;
A6: dom p = Seg 64 & dom q =Seg 64 by A4,A5,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p; then
i=1 or ... or i=64 by A6,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A6;
end;
end;
definition
func DES-PIPINV ->
Function of 64-tuples_on BOOLEAN,64-tuples_on BOOLEAN means :Def17:
for i be Element of 64-tuples_on BOOLEAN holds it.i = DES-IPINV(i);
existence
proof
deffunc F(Element of 64-tuples_on BOOLEAN) = DES-IPINV($1);
A1: for x being Element of 64-tuples_on BOOLEAN holds
F(x) is Element of 64-tuples_on BOOLEAN;
consider f being
Function of 64-tuples_on BOOLEAN, 64-tuples_on BOOLEAN such that
A2: for x being Element of 64-tuples_on BOOLEAN holds f.x = F(x)
from FUNCT_2:sch 9(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of 64-tuples_on BOOLEAN,64-tuples_on BOOLEAN;
assume A3:
for i be Element of 64-tuples_on BOOLEAN holds
f.i= DES-IPINV(i);
assume A4:
for i be Element of 64-tuples_on BOOLEAN holds
g.i= DES-IPINV(i);
for i be object st i in 64-tuples_on BOOLEAN holds f.i=g.i
proof
let i be object;
assume i in 64-tuples_on BOOLEAN;
then reconsider i as Element of 64-tuples_on BOOLEAN;
f.i=DES-IPINV(i) by A3
.=g.i by A4;
hence thesis;
end;
hence thesis;
end;
end;
Lm5:
for x be Element of 64-tuples_on BOOLEAN holds
DES-IPINV(DES-IP(x)) =x
proof
let x be Element of 64-tuples_on BOOLEAN;
set y =DES-IP(x);
set z= DES-IPINV(y);
len x =64&len z =64 by CARD_1:def 7;then
A1: dom x =Seg 64 &dom z=Seg 64 by FINSEQ_1:def 3;
A2:
z.1=y.40 & z.2=y.8 & z.3=y.48 & z.4=y.16 &
z.5=y.56 &z.6=y.24 & z.7=y.64 & z.8=y.32 &
z.9=y.39 & z.10=y.7 &z.11=y.47 & z.12=y.15 &
z.13=y.55 & z.14=y.23 & z.15=y.63 &z.16=y.31 &
z.17=y.38 & z.18=y.6 & z.19=y.46 & z.20=y.14 &
z.21=y.54 & z.22=y.22 & z.23=y.62 & z.24=y.30 &
z.25=y.37 &z.26=y.5 & z.27=y.45 & z.28=y.13 &
z.29=y.53 & z.30=y.21 &z.31=y.61 & z.32=y.29 &
z.33=y.36 & z.34=y.4 & z.35=y.44 &z.36=y.12 &
z.37=y.52 & z.38=y.20 & z.39=y.60 & z.40=y.28 &
z.41=y.35 & z.42=y.3 & z.43=y.43 & z.44=y.11 &
z.45=y.51 &z.46=y.19 & z.47=y.59 & z.48=y.27 &
z.49=y.34 & z.50=y.2 &z.51=y.42 & z.52=y.10 &
z.53=y.50 & z.54=y.18 & z.55=y.58 &z.56=y.26 &
z.57=y.33 & z.58=y.1 & z.59=y.41 & z.60=y.9 &
z.61=y.49 & z.62=y.17 & z.63=y.57 & z.64=y.25 by Def16;
for i be object st i in Seg 64 holds z.i=x.i
proof
let i be object;
assume i in Seg 64; then
i=1 or ... or i=64 by FINSEQ_1:91;
hence thesis by A2,Def14;
end;
hence thesis by A1;
end;
Lm6:
for x be Element of 64-tuples_on BOOLEAN holds
DES-IP(DES-IPINV(x)) =x
proof
let x be Element of 64-tuples_on BOOLEAN;
set y =DES-IPINV(x);
set z= DES-IP(y);
len x =64&len z =64 by CARD_1:def 7;then
A1: dom x =Seg 64 &dom z=Seg 64 by FINSEQ_1:def 3;
A2:
z.1=y.58 &z.2=y.50& z.3=y.42 & z.4=y.34 & z.5=y.26 &
z.6=y.18 & z.7=y.10 & z.8=y.2 & z.9=y.60 & z.10=y.52 &
z.11=y.44 & z.12=y.36 & z.13=y.28 & z.14=y.20 & z.15=y.12 &
z.16=y.4 & z.17=y.62 & z.18=y.54 & z.19=y.46 & z.20=y.38 &
z.21=y.30 & z.22=y.22 & z.23=y.14 & z.24=y.6 & z.25=y.64 &
z.26=y.56 & z.27=y.48 & z.28=y.40 & z.29=y.32 & z.30=y.24 &
z.31=y.16 & z.32=y.8 & z.33=y.57 & z.34=y.49 & z.35=y.41 &
z.36=y.33 & z.37=y.25 & z.38=y.17 & z.39=y.9 & z.40=y.1 &
z.41=y.59 & z.42=y.51 & z.43=y.43 & z.44=y.35 & z.45=y.27 &
z.46=y.19 & z.47=y.11 & z.48=y.3 & z.49=y.61 & z.50=y.53 &
z.51=y.45 & z.52=y.37 & z.53=y.29 & z.54=y.21 & z.55=y.13 &
z.56=y.5 & z.57=y.63 & z.58=y.55 & z.59=y.47 & z.60=y.39 &
z.61=y.31 & z.62=y.23 & z.63=y.15 & z.64=y.7 by Def14;
for i be object st i in Seg 64 holds z.i=x.i
proof
let i be object;
assume i in Seg 64; then
i=1 or ... or i=64 by FINSEQ_1:91;
hence thesis by A2,Def16;
end;
hence thesis by A1;
end;
Lm7:
DES-PIPINV * DES-PIP = id (64-tuples_on BOOLEAN)
proof
A1: dom(DES-PIPINV*DES-PIP)
= 64-tuples_on BOOLEAN by FUNCT_2:def 1;
for x be object st x in 64-tuples_on BOOLEAN holds
(DES-PIPINV*DES-PIP).x =x
proof
let x be object;
assume x in 64-tuples_on BOOLEAN;then
reconsider x as Element of 64-tuples_on BOOLEAN;
(DES-PIPINV*DES-PIP).x =DES-PIPINV.(DES-PIP.x) by FUNCT_2:15
.=DES-PIPINV.(DES-IP(x)) by Def15
.=DES-IPINV(DES-IP(x)) by Def17
.= x by Lm5;
hence thesis;
end;
hence thesis by A1,FUNCT_1:17;
end;
Lm8:
DES-PIP*DES-PIPINV = id (64-tuples_on BOOLEAN)
proof
A1: dom(DES-PIP*DES-PIPINV) = 64-tuples_on BOOLEAN by FUNCT_2:def 1;
for x be object st x in 64-tuples_on BOOLEAN holds
(DES-PIP*DES-PIPINV).x =x
proof
let x be object;
assume x in 64-tuples_on BOOLEAN;then
reconsider x as Element of 64-tuples_on BOOLEAN;
(DES-PIP*DES-PIPINV).x =DES-PIP.(DES-PIPINV.x) by FUNCT_2:15
.=DES-PIP.(DES-IPINV(x)) by Def17
.=DES-IP(DES-IPINV(x)) by Def15
.= x by Lm6;
hence thesis;
end;
hence thesis by A1,FUNCT_1:17;
end;
registration
cluster DES-PIP -> bijective;
coherence
by Lm7,Lm8,FUNCT_2:23;
end;
registration
cluster DES-PIPINV -> bijective;
correctness
by Lm7,Lm8,FUNCT_2:23;
end;
theorem
DES-PIPINV=DES-PIP" by Lm7,FUNCT_2:60;
begin :: Feistel function
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 48-element &
e.1=r.32 & e.2=r.1 & e.3=r.2& e.4=r.3& e.5=r.4&
e.6=r.5& e.7=r.4 & e.8=r.5 & e.9=r.6 & e.10=r.7 &
e.11=r.8 & e.12=r.9& e.13=r.8 & e.14=r.9 & e.15=r.10 &
e.16=r.11 & e.17=r.12 & e.18=r.13& e.19=r.12 & e.20=r.13 &
e.21=r.14 & e.22=r.15 & e.23=r.16 & e.24=r.17& e.25=r.16 &
e.26=r.17 & e.27=r.18 & e.28=r.19 & e.29=r.20 & e.30=r.21&
e.31=r.20 & e.32=r.21 & e.33=r.22 & e.34=r.23 & e.35=r.24 &
e.36=r.25& e.37=r.24 & e.38=r.25 & e.39=r.26 & e.40=r.27 &
e.41=r.28 & e.42=r.29& e.43=r.28 & e.44=r.29 & e.45=r.30 &
e.46=r.31 & e.47=r.32 & e.48=r.1 by Th23;
len e =48 by A1;then
reconsider e as Element of 48-tuples_on BOOLEAN by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 48-tuples_on BOOLEAN;
assume A2:
p.1=r.32 & p.2=r.1 & p.3=r.2& p.4=r.3& p.5=r.4&
p.6=r.5& p.7=r.4 & p.8=r.5 & p.9=r.6 & p.10=r.7 &
p.11=r.8 & p.12=r.9& p.13=r.8 & p.14=r.9 & p.15=r.10 &
p.16=r.11 & p.17=r.12 & p.18=r.13& p.19=r.12 & p.20=r.13 &
p.21=r.14 & p.22=r.15 & p.23=r.16 & p.24=r.17& p.25=r.16 &
p.26=r.17 & p.27=r.18 & p.28=r.19 & p.29=r.20 & p.30=r.21&
p.31=r.20 & p.32=r.21 & p.33=r.22 & p.34=r.23 & p.35=r.24 &
p.36=r.25& p.37=r.24 & p.38=r.25 & p.39=r.26 & p.40=r.27 &
p.41=r.28 & p.42=r.29& p.43=r.28 & p.44=r.29 & p.45=r.30 &
p.46=r.31 & p.47=r.32 & p.48=r.1;
assume A3:
q.1=r.32 & q.2=r.1 & q.3=r.2& q.4=r.3& q.5=r.4&
q.6=r.5& q.7=r.4 & q.8=r.5 & q.9=r.6 & q.10=r.7 &
q.11=r.8 & q.12=r.9& q.13=r.8 & q.14=r.9 & q.15=r.10 &
q.16=r.11 & q.17=r.12 & q.18=r.13& q.19=r.12 & q.20=r.13 &
q.21=r.14 & q.22=r.15 & q.23=r.16 & q.24=r.17& q.25=r.16 &
q.26=r.17 & q.27=r.18 & q.28=r.19 & q.29=r.20 & q.30=r.21&
q.31=r.20 & q.32=r.21 & q.33=r.22 & q.34=r.23 & q.35=r.24 &
q.36=r.25& q.37=r.24 & q.38=r.25 & q.39=r.26 & q.40=r.27 &
q.41=r.28 & q.42=r.29& q.43=r.28 & q.44=r.29 & q.45=r.30 &
q.46=r.31 & q.47=r.32 & q.48=r.1;
p in { s where s is Element of BOOLEAN*: len s = 48 };
then consider t be Element of BOOLEAN* such that
A4: p=t &len t = 48;
q in { s where s is Element of BOOLEAN*: len s = 48 };
then consider s be Element of BOOLEAN* such that
A5: q=s & len s =48;
A6: dom p= Seg 48 & dom q =Seg 48 by A4,A5,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p;
then i=1 or ... or i=48 by A6,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A6;
end;
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 32-element &
e.1=r.16 &e.2=r.7 &e.3=r.20 &e.4=r.21&
e.5=r.29 &e.6=r.12 &e.7=r.28 &e.8=r.17&
e.9=r.1 &e.10=r.15 &e.11=r.23 &e.12=r.26&
e.13=r.5 &e.14=r.18 &e.15=r.31 &e.16=r.10&
e.17=r.2 &e.18=r.8 &e.19=r.24 &e.20=r.14&
e.21=r.32 &e.22=r.27 &e.23=r.3 &e.24=r.9&
e.25=r.19 &e.26=r.13 &e.27=r.30 &e.28=r.6&
e.29=r.22 &e.30=r.11 &e.31=r.4 &e.32=r.25 by Th22;
len e =32 by A1;then
reconsider e as Element of 32-tuples_on BOOLEAN by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 32-tuples_on BOOLEAN;
assume A2:
p.1=r.16 &p.2=r.7 &p.3=r.20 &p.4=r.21&
p.5=r.29 &p.6=r.12 &p.7=r.28 &p.8=r.17&
p.9=r.1 &p.10=r.15 &p.11=r.23 &p.12=r.26&
p.13=r.5 &p.14=r.18 &p.15=r.31 &p.16=r.10&
p.17=r.2 &p.18=r.8 &p.19=r.24 &p.20=r.14&
p.21=r.32 &p.22=r.27 &p.23=r.3 &p.24=r.9&
p.25=r.19 &p.26=r.13 &p.27=r.30 &p.28=r.6&
p.29=r.22 &p.30=r.11 &p.31=r.4 &p.32=r.25;
assume A3:
q.1=r.16 &q.2=r.7 &q.3=r.20 &q.4=r.21&
q.5=r.29 &q.6=r.12 &q.7=r.28 &q.8=r.17&
q.9=r.1 &q.10=r.15 &q.11=r.23 &q.12=r.26&
q.13=r.5 &q.14=r.18 &q.15=r.31 &q.16=r.10&
q.17=r.2 &q.18=r.8 &q.19=r.24 &q.20=r.14&
q.21=r.32 &q.22=r.27 &q.23=r.3 &q.24=r.9&
q.25=r.19 &q.26=r.13 &q.27=r.30 &q.28=r.6&
q.29=r.22 &q.30=r.11 &q.31=r.4 &q.32=r.25;
p in { s where s is Element of BOOLEAN*: len s = 32 };
then consider t be Element of BOOLEAN* such that
A4: p=t &len t = 32;
q in { s where s is Element of BOOLEAN*: len s = 32 };
then consider s be Element of BOOLEAN* such that
A5: q=s & len s =32;
A6: dom p= Seg 32 & dom q =Seg 32 by A4,A5,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p;
then i=1 or ... or i=32 by A6,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A6;
end;
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
proof
r in { s where s is Element of BOOLEAN*: len s = 48};
then consider s be Element of BOOLEAN* such that
A1: r=s &len s = 48;
6<=len r & 42 = (len r) -6&
12<=len r & 36 = (len r) -12&
18<=len r & 30 = (len r) -18&
24<=len r & 24 = (len r) -24&
30<=len r & 18 = (len r) -30&
36<=len r & 12 = (len r) -36&
42<=len r& 6 = (len r) -42 by A1;
then A2:
len (Op-Right(r,6)) = 42 &
len (Op-Right(r,12)) = 36 &
len (Op-Right(r,18)) = 30 &
len (Op-Right(r,24)) = 24 &
len (Op-Right(r,30)) = 18 &
len (Op-Right(r,36)) = 12 &
len (Op-Right(r,42)) = 6 by RFINSEQ:def 1;
then A3:
len Op-Left(r,6) =6&
len Op-Left(Op-Right(r,6),6) =6&
len Op-Left(Op-Right(r,12),6) =6&
len Op-Left(Op-Right(r,18),6) =6&
len Op-Left(Op-Right(r,24),6) =6&
len Op-Left(Op-Right(r,30),6) =6&
len Op-Left(Op-Right(r,36),6) =6 by A1,FINSEQ_1:59;
reconsider x1=Op-Left(r,6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x2 = Op-Left(Op-Right(r,6),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x3 = Op-Left(Op-Right(r,12),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x4 = Op-Left(Op-Right(r,18),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x5=Op-Left(Op-Right(r,24),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x6 = Op-Left(Op-Right(r,30),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x7= Op-Left(Op-Right(r,36),6)
as Element of 6-tuples_on BOOLEAN by A3,FINSEQ_2:92;
reconsider x8 = Op-Right(r,42)
as Element of 6-tuples_on BOOLEAN by A2,FINSEQ_2:92;
set T1 =<*x1,x2,x3,x4*>;
set T2 =<*x5,x6,x7,x8*>;
set T = T1^T2;
A4: T.1=T1.1 & ... & T.4=T1.4 by FINSEQ_3:154;
A5: T.(4+1)=T2.1 &... & T.(4+4)=T2.4 by FINSEQ_3:155;
len T =8 & T is FinSequence of 6-tuples_on BOOLEAN by CARD_1:def 7;
then
reconsider T as Element of 8-tuples_on (6-tuples_on BOOLEAN)
by FINSEQ_2:92;
take T;
thus thesis by A4,A5;
end;
uniqueness
proof
let p,q be Element of 8-tuples_on (6-tuples_on BOOLEAN);
assume A6:
p.1 =Op-Left(r,6) &
p.2 =Op-Left(Op-Right(r,6),6) &
p.3 =Op-Left(Op-Right(r,12),6) &
p.4 =Op-Left(Op-Right(r,18),6) &
p.5 =Op-Left(Op-Right(r,24),6) &
p.6 =Op-Left(Op-Right(r,30),6) &
p.7 =Op-Left(Op-Right(r,36),6) &
p.8 =Op-Right(r,42);
assume A7:
q.1 =Op-Left(r,6) &
q.2 =Op-Left(Op-Right(r,6),6) &
q.3 =Op-Left(Op-Right(r,12),6) &
q.4 =Op-Left(Op-Right(r,18),6) &
q.5 =Op-Left(Op-Right(r,24),6) &
q.6 =Op-Left(Op-Right(r,30),6) &
q.7 =Op-Left(Op-Right(r,36),6) &
q.8 =Op-Right(r,42);
p in { s where s is Element of (6-tuples_on BOOLEAN)*: len s = 8};
then consider t be Element of (6-tuples_on BOOLEAN)* such that
A8: p=t &len t = 8;
q in { s where s is Element of (6-tuples_on BOOLEAN)*: len s = 8};
then consider s be Element of (6-tuples_on BOOLEAN)* such that
A9: q=s &len s = 8;
A10: dom p= Seg 8 & dom q =Seg 8 by A8,A9,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p; then
i=1 or i=2 or i=3 or i=4 or i=5 or i=6 or i=7 or i=8
by A10,ENUMSET1:def 6,FINSEQ_3:6;
hence thesis by A6,A7;
end;
hence thesis by A10;
end;
end;
theorem Th29:
for r be Element of 48-tuples_on BOOLEAN
ex s1,s2,s3,s4,s5,s6,s7,s8
be Element of 6-tuples_on BOOLEAN st
s1=(DES-DIV8(r)).1&
s2=(DES-DIV8(r)).2&
s3=(DES-DIV8(r)).3&
s4=(DES-DIV8(r)).4&
s5=(DES-DIV8(r)).5&
s6=(DES-DIV8(r)).6&
s7=(DES-DIV8(r)).7&
s8=(DES-DIV8(r)).8&
r=s1^s2^s3^s4^s5^s6^s7^s8
proof
let r be Element of 48-tuples_on BOOLEAN;
r is Element of Funcs(Seg 48,BOOLEAN) by FINSEQ_2:93;
then
dom r =Seg 48 by FUNCT_2:def 1;then
A1: len r =48 by FINSEQ_1:def 3;
1 in Seg 8;then
reconsider SEG8E1=1 as Element of Seg 8;
2 in Seg 8;then
reconsider SEG8E2=2 as Element of Seg 8;
3 in Seg 8;then
reconsider SEG8E3=3 as Element of Seg 8;
4 in Seg 8;then
reconsider SEG8E4=4 as Element of Seg 8;
5 in Seg 8;then
reconsider SEG8E5=5 as Element of Seg 8;
6 in Seg 8;then
reconsider SEG8E6=6 as Element of Seg 8;
7 in Seg 8;then
reconsider SEG8E7=7 as Element of Seg 8;
8 in Seg 8;then
reconsider SEG8E8=8 as Element of Seg 8;
set s1=(DES-DIV8(r)).SEG8E1,
s2=(DES-DIV8(r)).SEG8E2,
s3=(DES-DIV8(r)).SEG8E3,
s4=(DES-DIV8(r)).SEG8E4,
s5=(DES-DIV8(r)).SEG8E5,
s6=(DES-DIV8(r)).SEG8E6,
s7=(DES-DIV8(r)).SEG8E7,
s8=(DES-DIV8(r)).SEG8E8;
take s1,s2,s3,s4,s5,s6,s7,s8;
r=s1^s2^s3^s4^s5^s6^s7^s8
proof
A2:
s1 =Op-Left(r,6) &
s2 =Op-Left(Op-Right(r,6),6) &
s3 =Op-Left(Op-Right(r,12),6) &
s4 =Op-Left(Op-Right(r,18),6) &
s5 =Op-Left(Op-Right(r,24),6) &
s6 =Op-Left(Op-Right(r,30),6) &
s7 =Op-Left(Op-Right(r,36),6) &
s8 =Op-Right(r,42) by Def20;
s1^s2=r|12 by Th18,A1,A2;then
s1^s2^s3
=r|18 by Th18,A1,A2;then
s1^s2^s3^s4
=r|24 by Th18,A1,A2;then
s1^s2^s3^s4^s5
=r|30 by Th18,A1,A2;then
s1^s2^s3^s4^s5^s6
=r|36 by Th18,A1,A2;then
s1^s2^s3^s4^s5^s6^s7
=r|42 by Th18,A1,A2;
hence thesis by A2,RFINSEQ:8;
end;
hence thesis;
end;
Lm9:
for n be Nat, b be Element of BOOLEAN holds n*b <= n
proof
let n be Nat, b be Element of BOOLEAN;
b = 0 or b = 1 by TARSKI:def 2;
hence thesis;
end;
definition
let t be Element of 6-tuples_on BOOLEAN;
func B6toN64(t) -> Element of Segm 64 equals
32*(t.1) + 16*(t.6) + 8*(t.2) + 4*(t.3) + 2*(t.4) + 1*(t.5);
coherence
proof
A1:
32*(t.1) <= 32 & 16*(t.6)<=16 &8*(t.2)<=8 &
4*(t.3)<=4 &2*(t.4)<=2 &1*(t.5)<=1 by Lm9;
then
32*(t.1) + 16*(t.6) <= 32+16 by XREAL_1:7;then
32*(t.1) + 16*(t.6) + 8*(t.2)
<=48+8 by A1,XREAL_1:7;then
32*(t.1) + 16*(t.6) +
8*(t.2)+4*(t.3)<=56+4 by A1,XREAL_1:7;then
32*(t.1) + 16*(t.6) +
8*(t.2)+4*(t.3) +2*(t.4)<= 60+2 by A1,XREAL_1:7;then
32*(t.1) + 16*(t.6) + 8*(t.2)+
4*(t.3) +2*(t.4) +1*(t.5)<=62+1 by A1,XREAL_1:7;then
32*(t.1) + 16*(t.6) + 8*(t.2)
+4*(t.3)+2*(t.4)+1*(t.5) < 63+1 by XREAL_1:145;
hence thesis by NAT_1:44;
end;
end;
definition let a be Element of 16;
func N16toB4 a -> Tuple of 4,BOOLEAN equals
<*FALSE,FALSE,FALSE,FALSE*> if a = 0,
<*FALSE,FALSE,FALSE,TRUE*> if a = 1,
<*FALSE,FALSE,TRUE,FALSE*> if a = 2,
<*FALSE,FALSE,TRUE,TRUE*> if a = 3,
<*FALSE,TRUE,FALSE,FALSE*> if a = 4,
<*FALSE,TRUE,FALSE,TRUE*> if a = 5,
<*FALSE,TRUE,TRUE,FALSE*> if a = 6,
<*FALSE,TRUE,TRUE,TRUE*> if a = 7,
<*TRUE,FALSE,FALSE,FALSE*> if a = 8,
<*TRUE,FALSE,FALSE,TRUE*> if a = 9,
<*TRUE,FALSE,TRUE,FALSE*> if a = 10,
<*TRUE,FALSE,TRUE,TRUE*> if a = 11,
<*TRUE,TRUE,FALSE,FALSE*> if a = 12,
<*TRUE,TRUE,FALSE,TRUE*> if a = 13,
<*TRUE,TRUE,TRUE,FALSE*> if a = 15,
<*TRUE,TRUE,TRUE,TRUE*> if a = 16;
coherence;
consistency;
end;
definition
let R be Element of 32-tuples_on BOOLEAN,
RKey be Element of 48-tuples_on BOOLEAN;
func DES-F(R,RKey) -> Element of 32-tuples_on BOOLEAN means
ex D1,D2,D3,D4,D5,D6,D7,D8 be Element of 6-tuples_on BOOLEAN,
x1,x2,x3,x4,x5,x6,x7,x8 be Element of 4-tuples_on BOOLEAN,
C32 be 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
proof
consider
D1,D2,D3,D4,D5,D6,D7,D8 be Element of 6-tuples_on BOOLEAN such that
A1:
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
by Th29;
reconsider x1=N16toB4 (DES-SBOX1.(B6toN64(D1)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x2=N16toB4 (DES-SBOX2.(B6toN64(D2)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x3=N16toB4 (DES-SBOX3.(B6toN64(D3)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x4=N16toB4 (DES-SBOX4.(B6toN64(D4)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x5=N16toB4 (DES-SBOX5.(B6toN64(D5)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x6=N16toB4 (DES-SBOX6.(B6toN64(D6)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x7=N16toB4 (DES-SBOX7.(B6toN64(D7)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
reconsider x8=N16toB4 (DES-SBOX8.(B6toN64(D8)))
as Element of 4-tuples_on BOOLEAN by FINSEQ_2:131;
len (x1^x2^x3^x4^x5^x6^x7^x8) = 32 by CARD_1:def 7;then
x1^x2^x3^x4^x5^x6^x7^x8 is
Element of 32-tuples_on BOOLEAN by FINSEQ_2:92;
then
consider FIT be Element of 32-tuples_on BOOLEAN such that
A2: FIT = x1^x2^x3^x4^x5^x6^x7^x8;
reconsider PFIT=DES-P(FIT) as Element of 32-tuples_on BOOLEAN;
take PFIT;
thus thesis by A1,A2;
end;
uniqueness;
end;
definition
func DES-FFUNC ->
Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN
means
for z be Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:]
holds it.z = DES-F(z`1 ,z`2);
existence
proof
deffunc F(Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:])
=DES-F($1`1,$1`2);
A1: for x being Element of [:32-tuples_on BOOLEAN,48-tuples_on
BOOLEAN:]
holds
F(x) is Element of 32-tuples_on BOOLEAN;
consider f being
Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN
such that
A2: for x being Element of [:32-tuples_on BOOLEAN,48-tuples_on
BOOLEAN:]
holds f.x = F(x)
from FUNCT_2:sch 9(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN;
assume A3:
for i be Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:] holds
f.i= DES-F(i`1 ,i`2);
assume A4:
for i be Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:] holds
g.i= DES-F(i`1 ,i`2);
for i be Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:]
holds f.i=g.i
proof
let i be Element of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:];
thus
f.i=DES-F(i`1 ,i`2) by A3
.=g.i by A4;
end;
hence thesis;
end;
end;
begin :: Key Schedule
definition
let r be Element of 64-tuples_on BOOLEAN;
func DES-PC1(r) -> Element of 56-tuples_on BOOLEAN
means
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 56-element &
e.1=r.57&e.2=r.49&e.3=r.41&e.4=r.33&e.5=r.25&
e.6=r.17&e.7=r.9&e.8=r.1&e.9=r.58&e.10=r.50&
e.11=r.42&e.12=r.34&e.13=r.26&e.14=r.18&e.15=r.10&
e.16=r.2&e.17=r.59&e.18=r.51&e.19=r.43&e.20=r.35&
e.21=r.27&e.22=r.19&e.23=r.11&e.24=r.3&e.25=r.60&
e.26=r.52&e.27=r.44&e.28=r.36&e.29=r.63&e.30=r.55&
e.31=r.47&e.32=r.39&e.33=r.31&e.34=r.23&e.35=r.15&
e.36=r.7&e.37=r.62&e.38=r.54&e.39=r.46&e.40=r.38&
e.41=r.30&e.42=r.22&e.43=r.14&e.44=r.6&e.45=r.61&
e.46=r.53&e.47=r.45&e.48=r.37&e.49=r.29&e.50=r.21&
e.51=r.13&e.52=r.5&e.53=r.28&e.54=r.20&e.55=r.12&
e.56=r.4 by Th24;
len e =56 by A1;then
reconsider e as Element of 56-tuples_on BOOLEAN
by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 56-tuples_on BOOLEAN;
assume A2:
p.1=r.57&p.2=r.49&p.3=r.41&p.4=r.33&p.5=r.25&
p.6=r.17&p.7=r.9&p.8=r.1&p.9=r.58&p.10=r.50&
p.11=r.42&p.12=r.34&p.13=r.26&p.14=r.18&p.15=r.10&
p.16=r.2&p.17=r.59&p.18=r.51&p.19=r.43&p.20=r.35&
p.21=r.27&p.22=r.19&p.23=r.11&p.24=r.3&p.25=r.60&
p.26=r.52&p.27=r.44&p.28=r.36&p.29=r.63&p.30=r.55&
p.31=r.47&p.32=r.39&p.33=r.31&p.34=r.23&p.35=r.15&
p.36=r.7&p.37=r.62&p.38=r.54&p.39=r.46&p.40=r.38&
p.41=r.30&p.42=r.22&p.43=r.14&p.44=r.6&p.45=r.61&
p.46=r.53&p.47=r.45&p.48=r.37&p.49=r.29&p.50=r.21&
p.51=r.13&p.52=r.5&p.53=r.28&p.54=r.20&p.55=r.12&
p.56=r.4;
assume A3:
q.1=r.57&q.2=r.49&q.3=r.41&q.4=r.33&q.5=r.25&
q.6=r.17&q.7=r.9&q.8=r.1&q.9=r.58&q.10=r.50&
q.11=r.42&q.12=r.34&q.13=r.26&q.14=r.18&q.15=r.10&
q.16=r.2&q.17=r.59&q.18=r.51&q.19=r.43&q.20=r.35&
q.21=r.27&q.22=r.19&q.23=r.11&q.24=r.3&q.25=r.60&
q.26=r.52&q.27=r.44&q.28=r.36&q.29=r.63&q.30=r.55&
q.31=r.47&q.32=r.39&q.33=r.31&q.34=r.23&q.35=r.15&
q.36=r.7&q.37=r.62&q.38=r.54&q.39=r.46&q.40=r.38&
q.41=r.30&q.42=r.22&q.43=r.14&q.44=r.6&q.45=r.61&
q.46=r.53&q.47=r.45&q.48=r.37&q.49=r.29&q.50=r.21&
q.51=r.13&q.52=r.5&q.53=r.28&q.54=r.20&q.55=r.12&
q.56=r.4;
p in { s where s is Element of BOOLEAN*: len s = 56 };
then
A4: ex t be Element of BOOLEAN* st p = t & len t = 56;
q in { s where s is Element of BOOLEAN*: len s = 56 };
then ex s be Element of BOOLEAN* st q = s & len s = 56;
then
A5: dom p = Seg 56 & dom q =Seg 56 by A4,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p; then
i=1 or ... or i=56 by A5,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A5;
end;
end;
definition
let r be Element of 56-tuples_on BOOLEAN;
func DES-PC2(r) -> Element of 48-tuples_on BOOLEAN
means
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
proof
consider e be FinSequence of BOOLEAN such that
A1: e is 48-element &
e.1=r.14&e.2=r.17&e.3=r.11&e.4=r.24&e.5=r.1&
e.6=r.5&e.7=r.3&e.8=r.28&e.9=r.15&e.10=r.6&
e.11=r.21&e.12=r.10&e.13=r.23&e.14=r.19&
e.15=r.12&e.16=r.4&e.17=r.26&e.18=r.8&
e.19=r.16&e.20=r.7&e.21=r.27&e.22=r.20&
e.23=r.13&e.24=r.2&e.25=r.41&e.26=r.52&
e.27=r.31&e.28=r.37&e.29=r.47&e.30=r.55&
e.31=r.30&e.32=r.40&e.33=r.51&e.34=r.45&
e.35=r.33&e.36=r.48&e.37=r.44&e.38=r.49&
e.39=r.39&e.40=r.56&e.41=r.34&e.42=r.53&
e.43=r.46&e.44=r.42&e.45=r.50&e.46=r.36&
e.47=r.29&e.48=r.32 by Th23;
len e =48 by A1;then
reconsider e as Element of 48-tuples_on BOOLEAN
by FINSEQ_2:92;
take e;
thus thesis by A1;
end;
uniqueness
proof
let p,q be Element of 48-tuples_on BOOLEAN;
assume A2:
p.1=r.14&p.2=r.17&p.3=r.11&p.4=r.24&p.5=r.1&
p.6=r.5&p.7=r.3&p.8=r.28&p.9=r.15&p.10=r.6&
p.11=r.21&p.12=r.10&p.13=r.23&p.14=r.19&
p.15=r.12&p.16=r.4&p.17=r.26&p.18=r.8&
p.19=r.16&p.20=r.7&p.21=r.27&p.22=r.20&
p.23=r.13&p.24=r.2&p.25=r.41&p.26=r.52&
p.27=r.31&p.28=r.37&p.29=r.47&p.30=r.55&
p.31=r.30&p.32=r.40&p.33=r.51&p.34=r.45&
p.35=r.33&p.36=r.48&p.37=r.44&p.38=r.49&
p.39=r.39&p.40=r.56&p.41=r.34&p.42=r.53&
p.43=r.46&p.44=r.42&p.45=r.50&p.46=r.36&
p.47=r.29&p.48=r.32;
assume A3:
q.1=r.14&q.2=r.17&q.3=r.11&q.4=r.24&q.5=r.1&
q.6=r.5&q.7=r.3&q.8=r.28&q.9=r.15&q.10=r.6&
q.11=r.21&q.12=r.10&q.13=r.23&q.14=r.19&
q.15=r.12&q.16=r.4&q.17=r.26&q.18=r.8&
q.19=r.16&q.20=r.7&q.21=r.27&q.22=r.20&
q.23=r.13&q.24=r.2&q.25=r.41&q.26=r.52&
q.27=r.31&q.28=r.37&q.29=r.47&q.30=r.55&
q.31=r.30&q.32=r.40&q.33=r.51&q.34=r.45&
q.35=r.33&q.36=r.48&q.37=r.44&q.38=r.49&
q.39=r.39&q.40=r.56&q.41=r.34&q.42=r.53&
q.43=r.46&q.44=r.42&q.45=r.50&q.46=r.36&
q.47=r.29&q.48=r.32;
p in { s where s is Element of BOOLEAN*: len s = 48 };
then consider t be Element of BOOLEAN* such that
A4: p = t & len t = 48;
q in { s where s is Element of BOOLEAN*: len s = 48 };
then consider s be Element of BOOLEAN* such that
A5: q = s & len s = 48;
A6: dom p = Seg 48 & dom q =Seg 48 by A4,A5,FINSEQ_1:def 3;
for i be Nat st i in dom p holds p.i = q.i
proof
let i be Nat;
assume i in dom p; then
i=1 or ... or i=48 by A6,FINSEQ_1:91;
hence thesis by A2,A3;
end;
hence thesis by A6;
end;
end;
definition
func bitshift_DES -> FinSequence of NAT means
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 by Th21;
uniqueness
proof
let s,t be FinSequence of NAT;
assume A1:
s is 16-element &
s.1=1&s.2=1&s.3=2&s.4=2&
s.5=2&s.6=2&s.7=2&s.8=2&
s.9=1&s.10=2&s.11=2&s.12=2&
s.13=2&s.14=2&s.15=2&s.16=1;
then len s = 16;
then A2: dom s = Seg 16 by FINSEQ_1:def 3;
assume A3:
t is 16-element &
t.1=1&t.2=1&t.3=2&t.4=2&
t.5=2&t.6=2&t.7=2&t.8=2&
t.9=1&t.10=2&t.11=2&t.12=2&
t.13=2&t.14=2&t.15=2&t.16=1;
then len t = 16;
then A4: dom s = dom t by A2,FINSEQ_1:def 3;
for i be object st i in dom s holds s.i=t.i
proof
let i be object;
assume i in dom s; then
i=1 or ... or i=16 by A2,FINSEQ_1:91;
hence thesis by A1,A3;
end;
hence thesis by A4;
end;
end;
definition
let Key be Element of 64-tuples_on BOOLEAN;
func DES-KS(Key) -> Element of (16-tuples_on (48-tuples_on BOOLEAN)) means
ex C,D be 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 be 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
proof
defpred P[Nat,
Element of (28-tuples_on BOOLEAN ),
Element of (28-tuples_on BOOLEAN ),
Element of (28-tuples_on BOOLEAN ),
Element of (28-tuples_on BOOLEAN )]
means
$4 = Op-Shift($2,bitshift_DES.$1)
& $5 = Op-Shift($3,bitshift_DES.$1);
A1: for i being Nat,
z being Element of (28-tuples_on BOOLEAN ),
w being Element of (28-tuples_on BOOLEAN )
ex z1 being Element of (28-tuples_on BOOLEAN ),
w1 being Element of (28-tuples_on BOOLEAN )
st P[ i,z,w,z1, w1 ]
proof
let i being Nat,
z being Element of (28-tuples_on BOOLEAN ),
w being Element of (28-tuples_on BOOLEAN );
reconsider
z1= Op-Shift(z,bitshift_DES.i) as Element of (28-tuples_on BOOLEAN )
by Th14;
reconsider
w1= Op-Shift(w,bitshift_DES.i) as Element of (28-tuples_on BOOLEAN )
by Th14;
take z1,w1;
thus thesis;
end;
reconsider C0= Op-Left(DES-PC1(Key),28) as
Element of (28-tuples_on BOOLEAN ) by Th1;
DES-PC1(Key) is Element of 56-tuples_on BOOLEAN
& 28 <= 56 & 28=56-28;
then
reconsider D0 = Op-Right(DES-PC1(Key),28) as
Element of (28-tuples_on BOOLEAN ) by Th2;
consider
C,D be sequence of (28-tuples_on BOOLEAN )
such that
A2:
C.0=C0 & D.0= D0
& for n being Nat holds P[n,C.n,D.n,C.(n+1),D.(n+1)]
from RECDEF_2:sch 3(A1);
defpred PP[Nat,set] means
$2 = DES-PC2((C.$1)^(D.$1));
A3: for k be Nat st k in Seg 16 ex x being Element of
(48-tuples_on BOOLEAN) st PP[k,x];
consider OUT be FinSequence of (48-tuples_on BOOLEAN) such that
A4: dom OUT = Seg 16 & for j being Nat st j in Seg 16
holds PP[j,OUT.j] from FINSEQ_1:sch 5(A3);
len OUT = 16 by A4,FINSEQ_1:def 3;
then
reconsider OUT as Element of 16-tuples_on (48-tuples_on BOOLEAN)
by FINSEQ_2:92;
A5:
now let i be Element of NAT;
assume A6: 0<=i & i <=15;
A7: 0+1 <= i+1 by XREAL_1:6;
i +1 <=15 +1 by A6,XREAL_1:6;
then
i+1 in Seg 16 by A7;
hence
OUT.(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) by A2,A4;
end;
thus thesis by A5,A2;
end;
uniqueness
proof
let p,q be Element of (16-tuples_on ( 48-tuples_on BOOLEAN));
len p = 16 by CARD_1:def 7; then
A8:dom p =Seg 16 by FINSEQ_1:def 3;
q in { s where s is Element of
(48-tuples_on BOOLEAN)*: len s = 16 };
then consider s be Element of ( 48-tuples_on BOOLEAN)*
such that A9: q=s &len s = 16;
A10:dom q =Seg 16 by A9,FINSEQ_1:def 3;
given
C1,D1 be sequence of (28-tuples_on BOOLEAN )
such that A11:
C1.0= Op-Left(DES-PC1(Key),28) &
D1.0= Op-Right(DES-PC1(Key),28)
& (for i be Element of NAT
st 0<=i & i <=15
holds
p.(i+1)=DES-PC2((C1.(i+1))^(D1.(i+1)))
&
C1.(i+1) = Op-Shift(C1.i,bitshift_DES.i)
&
D1.(i+1) = Op-Shift(D1.i,bitshift_DES.i));
given
C2,D2 be sequence of (28-tuples_on BOOLEAN )
such that A12:
C2.0= Op-Left(DES-PC1(Key),28) &
D2.0= Op-Right(DES-PC1(Key),28)&
(for i be Element of NAT
st 0<=i & i <=15
holds
q.(i+1)=DES-PC2((C2.(i+1))^(D2.(i+1)))&
C2.(i+1) = Op-Shift(C2.i,bitshift_DES.i)&
D2.(i+1) = Op-Shift(D2.i,bitshift_DES.i));
defpred P[Nat] means
(0<=$1 & $1 <=15) implies p.($1+1) = q.($1+1)
&
C1.($1+1) = C2.($1+1) & D1.($1+1) = D2.($1+1);
A13: P[0]
proof
A14:C1.(0+1)
=Op-Shift(C2.0,bitshift_DES.0) by A11,A12
.=C2.(0+1) by A12;
A15:D1.(0+1) = Op-Shift(D2.0,bitshift_DES.0)
by A11,A12
.=D2.(0+1) by A12;
p.(0+1) =DES-PC2((C2.(0+1))^(D2.(0+1)))
by A14,A15,A11
.=q.(0+1) by A12;
hence thesis by A14,A15;
end;
A16: now let i be Nat;
assume A17: P[i];
thus P[i+1]
proof
assume A18: 0<=i+1 & i+1 <=15;
A19:
i <= i+1 by NAT_1:12;
A20:C1.((i+1)+1)
=Op-Shift(C2.(i+1),bitshift_DES.(i+1))
by A19,A17,A18,A11,XXREAL_0:2
.=C2.((i+1)+1) by A12,A18;
A21:D1.((i+1)+1)
= Op-Shift(D2.(i+1),bitshift_DES.(i+1))
by A19,A17,A18,A11,XXREAL_0:2
.=D2.((i+1)+1) by A12,A18;
p.((i+1)+1)
=DES-PC2((C2.((i+1)+1))^(D2.((i+1)+1)))
by A20,A21,A11,A18
.=q.((i+1)+1) by A12,A18;
hence thesis by A20,A21;
end;
end;
A22:for i be Nat holds P[i] from NAT_1:sch 2(A13,A16);
for i be object st i in dom p holds p.i = q.i
proof
let i be object;
assume A23:i in dom p;
reconsider i as Element of NAT by A23;
A24:1 <= i & i <= 16 by A23,A8,FINSEQ_1:1;
then
reconsider y=i-1 as Element of NAT by NAT_1:21;
1-1<= i-1 & i-1 <= 16-1 by A24,XREAL_1:9;
then p.(y+1)=q.(y+1) by A22;
hence thesis;
end;
hence thesis by A8,A10;
end;
end;
begin :: Encryption and Decryption
Lm10:
for m,n,k be non zero Element of NAT,
RK be Element of k-tuples_on (m-tuples_on BOOLEAN),
F be Function of [:n-tuples_on BOOLEAN,m-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN,
IP be Permutation of (2*n)-tuples_on BOOLEAN,
M be Element of (2*n)-tuples_on BOOLEAN
ex OUT be Element of (2*n)-tuples_on BOOLEAN st
ex L,R be sequence of (n-tuples_on BOOLEAN) st
L.0= SP-Left(IP.M)
& R.0= SP-Right(IP.M)
& (for i be Nat st 0<=i & i <= k-1
holds L.(i+1)= R.i
& R.(i+1)= Op-XOR(L.i,F.(R.i,RK/.(i+1))))
& OUT= IP".((R.k )^(L.k ))
proof
let m,n,k be non zero Element of NAT,
RK be Element of k-tuples_on (m-tuples_on BOOLEAN),
F be Function of [:n-tuples_on BOOLEAN,m-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN,
IP be Permutation of (2*n)-tuples_on BOOLEAN,
M be Element of (2*n)-tuples_on BOOLEAN;
defpred P[Nat,
Element of (n-tuples_on BOOLEAN ),
Element of (n-tuples_on BOOLEAN ),
Element of (n-tuples_on BOOLEAN ),
Element of (n-tuples_on BOOLEAN ) ] means
$4= $3 & $5=Op-XOR($2,F.($3,RK/.($1+1)));
A1: for
k being Nat,
x being Element of (n-tuples_on BOOLEAN ),
y being Element of (n-tuples_on BOOLEAN )
ex x1 being Element of (n-tuples_on BOOLEAN ),
y1 being Element of (n-tuples_on BOOLEAN )
st P[k,x,y,x1,y1];
consider L,R be sequence of (n-tuples_on BOOLEAN) such that
A2:
L.0=SP-Left(IP.M) & R.0=SP-Right(IP.M)
& for n be Nat holds P[n,L.n,R.n,L.(n+1),R.(n+1)]
from RECDEF_2:sch 3(A1);
A3:for i be 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))) by A2;
reconsider RL=((R.k )^(L.k )) as
Element of (2*n)-tuples_on BOOLEAN by FINSEQ_2:131;
IP".RL is Element of (2*n)-tuples_on BOOLEAN;
hence thesis by A3,A2;
end;
definition
let n,m,k be non zero Element of NAT,
RK be Element of (k-tuples_on (m-tuples_on BOOLEAN)),
F be Function of [:n-tuples_on BOOLEAN,m-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN,
IP be Permutation of (2*n)-tuples_on BOOLEAN,
M be Element of (2*n)-tuples_on BOOLEAN;
func DES-like-CoDec(M,F,IP,RK) -> Element of (2*n)-tuples_on BOOLEAN means
:Def29:
ex L,R be sequence of (n-tuples_on BOOLEAN)
st
L.0= SP-Left(IP.M) & R.0= SP-Right(IP.M)
& (for i be 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 by Lm10;
uniqueness
proof
let p,q be Element of (2*n)-tuples_on BOOLEAN;
given L1,R1 be sequence of (n-tuples_on BOOLEAN)
such that A1:
L1.0= SP-Left(IP.M) &
R1.0= SP-Right(IP.M)
&
(for i be Nat st 0<=i & i <= k-1
holds
L1.(i+1)= R1.i
&
R1.(i+1)=Op-XOR(L1.i,F.(R1.i,RK/.(i+1))))
& p=IP". ((R1.k )^(L1.k ));
given L2,R2 be sequence of (n-tuples_on BOOLEAN) such that
A2: L2.0= SP-Left(IP.M) & R2.0= SP-Right(IP.M)
&
(for i be Nat st 0<=i & i <= k-1 holds L2.(i+1)= R2.i
&
R2.(i+1)=Op-XOR(L2.i,F.(R2.i,RK/.(i+1))))
& q=IP". ((R2.k )^(L2.k ));
reconsider KD =k-1 as Element of NAT by INT_1:3;
defpred P[Nat] means
(0<=$1 & $1 <= k-1) implies R1.($1+1) = R2.($1+1) & L1.($1+1) = L2.($1+1);
A3: P[0]
proof
A4: L1.(0+1)
=R2.0 by A1,A2
.=L2.(0+1) by A2;
R1.(0+1)
=Op-XOR(L2.0,F.(R2.0,RK/.(0+1))) by A1,A2
.=R2.(0+1) by A2;
hence thesis by A4;
end;
A5: now let i be Nat;
assume A6: P[i];
thus P[i+1]
proof
assume A7: 0<=i+1 & i+1 <=k-1;
A8:i <= i+1 by NAT_1:12;
A9: L1.((i+1)+1)
=R2.(i+1) by A7,A6,A8,A1,XXREAL_0:2
.=L2.((i+1)+1) by A2,A7;
R1.((i+1)+1)
=Op-XOR(L1.(i+1),F.(R1.(i+1),RK/.((i+1)+1))) by A1,A7;
hence thesis by A9,A2,A7,A6,A8,XXREAL_0:2;
end;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A5);
then P[KD];
hence thesis by A1,A2;
end;
end;
theorem Th30:
for n,m,k be non zero Element of NAT,
RK be Element of k-tuples_on (m-tuples_on BOOLEAN),
F be Function of [:n-tuples_on BOOLEAN,m-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN,
IP be Permutation of (2*n)-tuples_on BOOLEAN,
M be Element of (2*n)-tuples_on BOOLEAN holds
DES-like-CoDec(DES-like-CoDec(M,F,IP,RK),F,IP,Rev(RK))=M
proof
let n,m,k be non zero Element of NAT,
RK be Element of k-tuples_on (m-tuples_on BOOLEAN),
F be Function of [:n-tuples_on BOOLEAN,m-tuples_on BOOLEAN:],
n-tuples_on BOOLEAN,
IP be Permutation of (2*n)-tuples_on BOOLEAN,
M be Element of (2*n)-tuples_on BOOLEAN;
set REVRKS= Rev (RK);
set EM=DES-like-CoDec(M,F,IP,RK);
consider L,R be sequence of (n-tuples_on BOOLEAN) such that
A1:L.0= SP-Left(IP.M) & R.0= SP-Right(IP.M)
& (for i be 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)))) &
EM=IP".((R.k )^(L.k)) by Def29;
consider LB,RB be sequence of (n-tuples_on BOOLEAN) such that
A2: LB.0= SP-Left(IP.EM) & RB.0= SP-Right(IP.EM) &
(for i be Nat st 0<=i & i <=k-1 holds LB.(i+1)= RB.i &
RB.(i+1)=Op-XOR(LB.i,F.(RB.i,REVRKS/.(i+1))))
& DES-like-CoDec(EM,F,IP,REVRKS)
=IP". ((RB.k )^(LB.k )) by Def29;
defpred P[Nat] means $1 <=k implies
(LB.$1 = R.(k-$1) & RB.$1 = L.(k-$1) );
A3: P[0]
proof
A4: len (R.k) =n by CARD_1:def 7;
rng IP = (2*n)-tuples_on BOOLEAN by FUNCT_2:def 3;
then
A5:(R.k)^(L.k) in rng IP by FINSEQ_2:131;
A6: IP.EM = (R.k)^(L.k) by A5,A1,FUNCT_1:35;
A7: len (R.k) =n by CARD_1:def 7;
((R.k)^(L.k) )| n
= ((R.k)^(L.k) )| (dom (R.k)) by A4,FINSEQ_1:def 3
.= R.k by FINSEQ_1:21;
hence thesis by A2,A7,A6,FINSEQ_5:37;
end;
A8: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A9: P[i];
now assume
A10: i+1 <= k;
A11:i <= i+1 by NAT_1:11;
then
A12: i <= k by A10,XXREAL_0:2;
A13:(i+1)-(i+1) <= k -(i+1) by A10,XREAL_1:9;
A14:(k-1) - i <= (k-1)-0 by XREAL_1:13;
i-i <= k-i by A12,XREAL_1:9;
then
reconsider i16=k-i as Element of NAT by INT_1:3;
reconsider i161 = k-(i+1) as Element of NAT
by A13,INT_1:3;
A15:
i+1 -1 <= k-1 by A10,XREAL_1:9;
then
A16:
LB.(i+1)= RB.i &
RB.(i+1)=Op-XOR(LB.i,F.(RB.i,REVRKS/.(i+1))) by A2;
reconsider Ki=REVRKS/.(i+1)
as Element of m-tuples_on BOOLEAN;
A17: RB.i =L.(k-(i+1) +1 )
by A9,A10,A11,XXREAL_0:2
.=R.(i161) by A1,A14;
A18: len RK = k by CARD_1:def 7;
1<= (i+1) & (i+1) <=k by A10,NAT_1:11;
then
(i+1) in Seg k;
then
A19: (i+1) in dom RK by A18,FINSEQ_1:def 3;
then
A20: (i+1) in dom REVRKS by FINSEQ_5:57;
A21: k-i <= k-0 by XREAL_1:10;
k-(k-1) <= k-i by A15,XREAL_1:10;
then
i16 in Seg k by A21;
then
A22: (k -i) in dom RK by A18,FINSEQ_1:def 3;
A23: REVRKS/.(i+1)
= REVRKS.(i+1) by A20,PARTFUN1:def 6
.= RK.(len RK -(i+1) +1) by A19,FINSEQ_5:58
.= RK/.(k -i) by A22,A18,PARTFUN1:def 6;
LB.i=Op-XOR(L.(i161),F.(R.(i161),RK/.(i161+1)))
by A1,A14,A9,A10,A11,XXREAL_0:2
.=Op-XOR(L.(i161),F.(R.(i161),Ki)) by A23;
hence LB.(i+1) = R.(k-(i+1)) &
RB.(i+1) = L.(k-(i+1)) by A16,A17,Th17;
end;
hence thesis;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A8);
then
LB.k = R.(k-k) & RB.k = L.(k-k);then
(RB.k )^(LB.k ) = IP.M by Th3,A1;
hence thesis by A2,FUNCT_2:26;
end;
definition
let RK be Element of (16-tuples_on (48-tuples_on BOOLEAN)),
F be Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN,
IP be Permutation of 64-tuples_on BOOLEAN,
M be Element of 64-tuples_on BOOLEAN;
func DES-CoDec(M,F,IP,RK) -> Element of 64-tuples_on BOOLEAN
means :Def30:
ex IPX be Permutation of (2*32)-tuples_on BOOLEAN,
MX be Element of (2*32)-tuples_on BOOLEAN st
IPX=IP & MX =M & it =DES-like-CoDec(MX,F,IPX,RK);
existence
proof
reconsider IPX = IP as Permutation of (2*32)-tuples_on BOOLEAN;
reconsider MX = M as Element of (2*32)-tuples_on BOOLEAN;
reconsider CM =DES-like-CoDec(MX,F,IPX,RK)
as Element of 64-tuples_on BOOLEAN;
take CM;
thus thesis;
end;
uniqueness;
end;
theorem Th31:
for RK be Element of 16-tuples_on (48-tuples_on BOOLEAN),
F be Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN,
IP be Permutation of 64-tuples_on BOOLEAN,
M be Element of 64-tuples_on BOOLEAN holds
DES-CoDec(DES-CoDec(M,F,IP,RK),F,IP,Rev(RK))=M
proof
let RK be Element of 16-tuples_on (48-tuples_on BOOLEAN),
F be Function of [:32-tuples_on BOOLEAN,48-tuples_on BOOLEAN:],
32-tuples_on BOOLEAN,
IP be Permutation of 64-tuples_on BOOLEAN,
M be Element of 64-tuples_on BOOLEAN;
reconsider IPX = IP as Permutation of (2*32)-tuples_on BOOLEAN;
reconsider MX = M as Element of (2*32)-tuples_on BOOLEAN;
reconsider EM = DES-like-CoDec(MX,F,IPX,RK)
as Element of (2*32)-tuples_on BOOLEAN;
reconsider EM64 = DES-CoDec(M,F,IP,RK) as Element of 64-tuples_on BOOLEAN;
EM=EM64 by Def30;
then
DES-like-CoDec(EM,F,IPX,Rev(RK))
=DES-CoDec(EM64,F,IP,Rev(RK)) by Def30;
hence thesis by Th30;
end;
definition
let plaintext,secretkey be Element of 64-tuples_on BOOLEAN;
func DES-ENC(plaintext,secretkey) -> Element of 64-tuples_on BOOLEAN
equals
DES-CoDec (plaintext,DES-FFUNC,DES-PIP,DES-KS(secretkey));
correctness;
end;
definition
let ciphertext,secretkey be Element of 64-tuples_on BOOLEAN;
func DES-DEC(ciphertext,secretkey) -> Element of 64-tuples_on BOOLEAN
equals
DES-CoDec (ciphertext,DES-FFUNC,DES-PIP,Rev(DES-KS(secretkey)));
correctness;
end;
theorem
for message,secretkey be Element of 64-tuples_on BOOLEAN
holds DES-DEC(DES-ENC(message,secretkey),secretkey) = message by Th31;