Copyright (c) 1998 Association of Mizar Users
environ
vocabulary MIDSP_3, MARGREL1, FILTER_0, ARYTM_3, NAT_1, INT_1, ARYTM_1, POWER,
GRCAT_1, FINSEQ_2, BINARITH, FINSEQ_1, FUNCT_1, RELAT_1, BINARI_3,
CQC_LANG, MATRIX_1, INCSP_1, PRALG_1, FUNCT_7, FUNCT_2, FUNCT_5, BOOLE,
TREES_1, IDEA_1, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, INT_1, INT_2,
NAT_1, MARGREL1, RELAT_1, FUNCT_1, MATRIX_1, PRALG_1, PARTFUN1, FUNCT_2,
FUNCT_5, FUNCT_7, SERIES_1, CQC_LANG, FINSEQ_1, FINSEQ_2, FINSEQ_4,
BINARITH, BINARI_3, WSIERP_1, MIDSP_3;
constructors FUNCT_7, BINARI_2, SERIES_1, BINARITH, BINARI_3, FINSEQ_4,
WSIERP_1, INT_2, MEMBERED;
clusters INT_1, FUNCT_1, RELSET_1, MARGREL1, BINARITH, FUNCT_7, NAT_1,
XREAL_0, MEMBERED, FUNCT_2, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
theorems REAL_1, NAT_1, NAT_2, NAT_LAT, INT_1, INT_2, FINSEQ_1, FINSEQ_2,
FINSEQ_4, AXIOMS, FUNCT_1, FUNCT_2, FUNCT_5, FUNCT_7, PRALG_1, CQC_LANG,
POWER, GROUP_4, RLVECT_1, GR_CY_1, EULER_1, EULER_2, BINARITH, BINARI_3,
MATRIX_1, AMI_5, RELSET_1, RELAT_1, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes FINSEQ_1, FINSEQ_2, MATRIX_2, NAT_1, FUNCT_2;
begin ::Some selected theorems on integers
reserve i,j,k,n for Nat;
reserve x,y,z for Tuple of n, BOOLEAN;
Lm1: i<>0 & i < j & j is prime implies i,j are_relative_prime
proof
assume A1:i<>0 & i < j & j is prime;
now
set IJ = i hcf j;
IJ divides j by NAT_1:def 5;
then A2:IJ = 1 or IJ = j by A1,INT_2:def 5;
IJ <> j
proof
assume IJ = j;
then j divides i & j divides j by NAT_1:def 5;
then consider n being Nat such that
A3:i = j*n by NAT_1:def 3;
A4:j >= 0 by NAT_1:18;
j <> 0 & n <> 0 by A1,A3;
then n >= 1 by RLVECT_1:99;
then j*n >= j*1 by A4,AXIOMS:25;
hence contradiction by A1,A3;
end;
hence thesis by A2,INT_2:def 6;
end;
hence thesis;
end;
Lm2:
j is prime & i<j & k<j & i<>0 implies
ex a being Nat st (a*i) mod j = k
proof
assume that
A1: j is prime and
A2: i<j and
A3: k<j and
A4: i<>0;
j>1 by A1,INT_2:def 5;
then A5:j>0 by AXIOMS:22;
i,j are_relative_prime by A1,A2,A4,Lm1;
then consider a,b being Integer such that
A6:a*i + b*j = k by EULER_1:11;
now per cases;
suppose A7:a >= 0;
now per cases;
suppose b >= 0;
then reconsider a,b as Nat by A7,INT_1:16;
A8:(a*i + b*j) mod j = k by A3,A6,GR_CY_1:4;
A9: (a*i + b*j) mod j = (a*i + ((b*j) mod j)) mod j by GR_CY_1:3
.= (a*i + 0) mod j by GROUP_4:101
.= (a*i) mod j;
take a;
thus thesis by A8,A9;
suppose A10: b < 0;
reconsider a as Nat by A7,INT_1:16;
consider b' being Integer such that
A11:b'=0-b;
b - b < 0 - b by A10,REAL_1:54;
then 0 < 0 - b by XCMPLX_1:14;
then reconsider b' as Nat by A11,INT_1:16;
take a;
a*i + b*j + b'*j = a*i + (b*j + b'*j) by XCMPLX_1:1
.= a*i + (b + (0 - b))*j by A11,XCMPLX_1:8
.= a*i + (b + -b)*j by XCMPLX_1:150
.= a*i + 0*j by XCMPLX_0:def 6
.= a*i;
then (a*i) mod j = k mod j by A6,GR_CY_1:1
.= k by A3,GR_CY_1:4;
hence thesis;
end;
hence thesis;
suppose A12: a < 0;
consider a1 being Integer such that
A13:a1 = 0 - a;
A14: a1 = -a by A13,XCMPLX_1:150;
a - a < 0 - a by A12,REAL_1:54;
then 0 < 0 - a by XCMPLX_1:14;
then reconsider a1 as Nat by A13,INT_1:16;
consider a2 being Nat such that
A15:a2=(a1 div j) + 1;
consider a' being Integer such that
A16:a'=a + a2 * j;
A17:a' = a + ((a1 div j)*j + 1*j) by A15,A16,XCMPLX_1:8
.= -a1 + (a1 div j)*j + j by A14,XCMPLX_1:1;
consider t being Nat such that
A18: a1 = j * (a1 div j) + t & t < j by A5,NAT_1:def 1;
A19:a1 - (a1 + t) = a1 - a1 - t by XCMPLX_1:36
.= 0 - t by XCMPLX_1:14
.= -t by XCMPLX_1:150;
A20: j*(a1 div j) + t - (a1 + t)
= j*(a1 div j) + (t - (a1 + t)) by XCMPLX_1:29
.= j*(a1 div j) + (t - t - a1) by XCMPLX_1:36
.= j*(a1 div j) + (0 - a1) by XCMPLX_1:14
.= (a1 div j)*j + -a1 by XCMPLX_1:150;
-t + t < -t + j by A18,REAL_1:53;
then 0 < a' by A17,A18,A19,A20,XCMPLX_0:def 6;
then reconsider a' as Nat by INT_1:16;
now per cases;
suppose b >= 0;
then reconsider b as Nat by INT_1:16;
take a';
A21:a*i + b*j + a2*j*i
= a*i + a2*j*i + b*j by XCMPLX_1:1
.= a'*i + b*j by A16,XCMPLX_1:8;
(k + a2*j*i) mod j = (k + a2*i*j) mod j by XCMPLX_1:4
.= k mod j by GR_CY_1:1
.= k by A3,GR_CY_1:4;
hence (a'*i) mod j = k by A6,A21,GR_CY_1:1;
suppose A22: b < 0;
consider b' being Integer such that
A23:b'=0-b;
b - b < 0 - b by A22,REAL_1:54;
then 0 < b' by A23,XCMPLX_1:14;
then reconsider b' as Nat by INT_1:16;
take a';
A24: a*i + b*j + a2*j*i + b'*j
= a*i + (b*j + a2*j*i) + b'*j by XCMPLX_1:1
.= a*i + (a2*j*i + b*j + b'*j) by XCMPLX_1:1
.= a*i + (a2*j*i + (b*j + b'*j)) by XCMPLX_1:1
.= a*i + (a2*j*i + (b + (0 - b))*j) by A23,XCMPLX_1:8
.= a*i + (a2*j*i + (b + -b)*j) by XCMPLX_1:150
.= a*i + (a2*j*i + 0*j) by XCMPLX_0:def 6
.= a'*i by A16,XCMPLX_1:8;
k + a2*j*i + b'*j = k + a2*i*j + b'*j by XCMPLX_1:4
.= k + (a2*i*j + b'*j) by XCMPLX_1:1
.= k + (a2*i+ b')*j by XCMPLX_1:8;
hence (a'*i) mod j = k mod j by A6,A24,GR_CY_1:1
.= k by A3,GR_CY_1:4;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th1:
for i,j,k holds j is prime & i<j & k<j & i<>0 implies
ex a being Nat st (a*i) mod j = k & a < j
proof
let i,j,k be Nat;
assume A1: j is prime & i<j & k<j & i<>0;
then j>1 by INT_2:def 5;
then A2:j>0 by AXIOMS:22;
consider a being Nat such that
A3: (a*i) mod j = k by A1,Lm2;
consider a' being Nat such that
A4: a' = a mod j;
take a';
thus thesis by A2,A3,A4,EULER_2:10,NAT_1:46;
end;
theorem Th2:
for n,k1,k2 being Nat holds
n <> 0 & k1 mod n = k2 mod n & k1 <= k2 implies
ex t being Nat st k2 - k1 = n*t
proof
let n,k1,k2 be Nat;
assume A1: n <> 0 & k1 mod n = k2 mod n & k1 <= k2;
then A2: n>0 by NAT_1:19;
then k1 = n * (k1 div n) + (k1 mod n) by NAT_1:47;
then A3: k1 mod n = k1 - n * (k1 div n) by XCMPLX_1:26;
k2 = n * (k2 div n) + (k2 mod n) by A2,NAT_1:47;
then k2 - n * (k2 div n) = k1 - n * (k1 div n) by A1,A3,XCMPLX_1:26;
then k2 - (n * (k2 div n) - n * (k2 div n))
= k1 - n * (k1 div n) + n * (k2 div n) by XCMPLX_1:37;
then k2 - 0 = k1 - n * (k1 div n) + n * (k2 div n) by XCMPLX_1:14;
then A4: k2 = k1 + - n * (k1 div n) + n * (k2 div n) by XCMPLX_0:def 8
.= k1 + (- n * (k1 div n) + n * (k2 div n)) by XCMPLX_1:1
.= k1 + (n * (k2 div n) - n * (k1 div n)) by XCMPLX_0:def 8
.= k1 + (n * ((k2 div n) - (k1 div n))) by XCMPLX_1:40;
consider t being Integer such that
A5: t = (k2 div n) - (k1 div n);
(k2 div n) >= (k1 div n) by A1,NAT_2:26;
then (k2 div n) - (k1 div n) >= (k1 div n) - (k1 div n) by REAL_1:49;
then t >= 0 by A5,XCMPLX_1:14;
then reconsider t as Nat by INT_1:16;
take t;
thus k2 - k1 = n * t + (k1 - k1) by A4,A5,XCMPLX_1:29
.= n * t + 0 by XCMPLX_1:14
.= n * t;
end;
theorem Th3:
for a, b being Nat holds a - b <= a
proof
let a, b be Nat;
0 <= b by NAT_1:18;
then a - b <= a - 0 by REAL_1:92;
hence thesis;
end;
theorem Th4:
for b1,b2,c being Nat holds b2 <= c implies b2 - b1 <= c
proof
let b1,b2,c be Nat;
assume A1: b2 <= c;
A2: c - b1 <= c by Th3;
b2 - b1 <= c - b1 by A1,REAL_1:49;
hence b2 - b1 <= c by A2,AXIOMS:22;
end;
theorem Th5:
for a,b,c being Nat holds 0<a & 0<b & a<c & b<c & c is prime implies
(a * b) mod c <> 0
proof
let a,b,c be Nat;
assume A1: 0<a & 0<b & a<c & b<c & c is prime;
assume A2: (a * b) mod c = 0;
0 < c by A1,AXIOMS:22;
then (a * b) = c * ((a * b) div c) + 0 by A2,NAT_1:47;
then c divides (a * b) by NAT_1:def 3;
then c divides a or c divides b by A1,NAT_LAT:95;
hence contradiction by A1,NAT_1:54;
end;
theorem
for n being non empty Nat holds 2 to_power(n) <> 1
proof
let n be non empty Nat;
n > 0 by NAT_1:19;
hence thesis by POWER:40;
end;
begin :: Algebraic group on Fixed-length bit Integer
:: In this section,we construct an algebraic group on
:: Fixed-length bit Integer.
:: IDEA's Basic operators are 'xor', ADD_MOD and MUL_MOD.
:: 'xor' is 16-bitwise XOR. ADD_MOD is addition mod 2^{16}.
:: MUL_MOD is multiplication mod 2^(16)+1. And, we define
:: two functions NEG_MOD and INV_MOD that give inverse
:: element of ADD_MOD and MUL_MOD respectively.
definition
let n;
func ZERO( n ) -> Tuple of n, BOOLEAN equals
:Def1:
n |-> FALSE;
correctness by FINSEQ_2:132;
end;
definition
let n;
let x, y be Tuple of n, BOOLEAN;
func x 'xor' y -> Tuple of n, BOOLEAN means
:Def2:
for i st i in Seg n holds it/.i = (x/.i) 'xor' (y/.i);
existence
proof
deffunc F(Nat)=(x/.$1) 'xor' (y/.$1);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n, BOOLEAN by A1,FINSEQ_2:110;
take z;
let i;
assume A3: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by FINSEQ_4:def 4
.= (x/.i) 'xor' (y/.i) by A2,A3;
end;
uniqueness
proof
let z1, z2 be Tuple of n, BOOLEAN such that
A4: for i st i in Seg n holds z1/.i = (x/.i) 'xor' (y/.i) and
A5: for i st i in Seg n holds z2/.i = (x/.i) 'xor' (y/.i);
A6: len z1 = n & len z2 = n by FINSEQ_2:109;
now let j;
assume A7: j in Seg n;
then A8: j in dom z1 & j in dom z2 by A6,FINSEQ_1:def 3;
hence z1.j = z1/.j by FINSEQ_4:def 4
.= (x/.j) 'xor' (y/.j) by A4,A7
.= z2/.j by A5,A7
.= z2.j by A8,FINSEQ_4:def 4;
end;
hence z1 = z2 by A6,FINSEQ_2:10;
end;
end;
theorem Th7:
for n,x holds x 'xor' x = ZERO(n)
proof
let n;
let x be Tuple of n, BOOLEAN;
A1:len (x 'xor' x) = n & len (ZERO(n)) = n by FINSEQ_2:109;
now let j;
assume A2:j in Seg n;
then A3:j in dom (x 'xor' x) & j in dom (ZERO(n)) by A1,FINSEQ_1:def 3;
then j in dom (x 'xor' x) & j in dom (n |-> FALSE) by Def1;
then A4:j in dom (x 'xor' x) & j in Seg n by FINSEQ_2:68;
A5:ZERO(n).j = (n |-> FALSE).j by Def1
.= FALSE by A4,FINSEQ_2:70;
thus (x 'xor' x).j = (x 'xor' x)/.j by A3,FINSEQ_4:def 4
.= (x/.j) 'xor' (x/.j) by A2,Def2
.= ZERO(n).j by A5,BINARITH:15;
end;
hence thesis by A1,FINSEQ_2:10;
end;
theorem Th8:
for n,x,y holds x 'xor' y = y 'xor' x
proof
let n;
let x,y be Tuple of n, BOOLEAN;
A1:len (x 'xor' y) = n & len (y 'xor' x) = n by FINSEQ_2:109;
now let j;
assume A2:j in Seg n;
then A3:j in dom (x 'xor' y) & j in dom (y 'xor' x) by A1,FINSEQ_1:def 3;
hence (x 'xor' y).j = (x 'xor' y)/.j by FINSEQ_4:def 4
.= (y/.j) 'xor' (x/.j) by A2,Def2
.= (y 'xor' x)/.j by A2,Def2
.= (y 'xor' x).j by A3,FINSEQ_4:def 4;
end;
hence thesis by A1,FINSEQ_2:10;
end;
definition
let n;
let x, y be Tuple of n, BOOLEAN;
redefine func x 'xor' y;
commutativity by Th8;
end;
theorem Th9:
for n,x holds ZERO(n) 'xor' x = x
proof
let n;
let x be Tuple of n, BOOLEAN;
A1:len ((ZERO(n)) 'xor' x) = n & len x = n by FINSEQ_2:109;
now let j;
assume A2:j in Seg n;
then A3:j in dom ((ZERO(n)) 'xor' x) & j in dom x by A1,FINSEQ_1:def 3;
j in dom (ZERO(n))
proof
dom (ZERO(n)) = dom (n |-> FALSE) by Def1
.= Seg n by FINSEQ_2:68;
hence thesis by A2;
end;
then A4:(ZERO(n))/.j = ZERO(n).j by FINSEQ_4:def 4
.= (n |-> FALSE).j by Def1
.= FALSE by A2,FINSEQ_2:70;
thus ((ZERO(n)) 'xor' x).j = ((ZERO(n)) 'xor' x)/.j by A3,FINSEQ_4:def 4
.= FALSE 'xor' (x/.j) by A2,A4,Def2
.= x/.j by BINARITH:14
.= x.j by A3,FINSEQ_4:def 4;
end;
hence thesis by A1,FINSEQ_2:10;
end;
theorem Th10:
for n,x,y,z holds (x 'xor' y) 'xor' z = x 'xor' (y 'xor' z)
proof
let n;
let x,y,z be Tuple of n, BOOLEAN;
A1:len ((x 'xor' y) 'xor' z) = n &
len (x 'xor' (y 'xor' z)) = n by FINSEQ_2:109;
now let j;
assume A2:j in Seg n;
then A3:j in dom ((x 'xor' y) 'xor' z) &
j in dom (x 'xor' (y 'xor' z)) by A1,FINSEQ_1:def 3;
hence ((x 'xor' y) 'xor' z).j
= ((x 'xor' y) 'xor' z)/.j by FINSEQ_4:def 4
.= ((x 'xor' y)/.j) 'xor' (z/.j) by A2,Def2
.= ((x/.j) 'xor' (y/.j)) 'xor' (z/.j) by A2,Def2
.= (x/.j) 'xor' ((y/.j) 'xor' (z/.j)) by BINARITH:34
.= (x/.j) 'xor' ((y 'xor' z)/.j) by A2,Def2
.= ((x 'xor' (y 'xor' z)))/.j by A2,Def2
.= (x 'xor' (y 'xor' z)).j by A3,FINSEQ_4:def 4;
end;
hence thesis by A1,FINSEQ_2:10;
end;
definition
let n;
let i be Nat;
pred i is_expressible_by n means
:Def3: i < 2 to_power(n);
end;
theorem
for n holds n-BinarySequence 0 = ZERO(n)
proof
let n;
A1:len (n-BinarySequence 0) = n & len (ZERO(n)) = n by FINSEQ_2:109;
then A2:dom (n-BinarySequence 0) = Seg n &
dom ZERO(n) = Seg n by FINSEQ_1:def 3;
now let j;
assume A3: j in Seg n;
A4: (0 div 2 to_power(j-'1)) mod 2
= 0 mod 2 by NAT_2:4
.= 0 by GR_CY_1:6;
j in dom (ZERO(n))
proof
dom (ZERO(n)) = dom (n |-> FALSE) by Def1
.= Seg n by FINSEQ_2:68;
hence thesis by A3;
end;
then A5:(ZERO(n))/.j = ZERO(n).j by FINSEQ_4:def 4
.= (n |-> FALSE).j by Def1
.= FALSE by A3,FINSEQ_2:70;
thus (n-BinarySequence 0).j
= (n-BinarySequence 0)/.j by A2,A3,FINSEQ_4:def 4
.= IFEQ((0 div 2 to_power(j-'1)) mod 2,0,FALSE,TRUE)
by A3,BINARI_3:def 1
.= (ZERO(n))/.j by A4,A5,CQC_LANG:def 1
.= ZERO(n).j by A2,A3,FINSEQ_4:def 4;
end;
hence thesis by A1,FINSEQ_2:10;
end;
definition
let n;
let i, j be Nat;
func ADD_MOD(i,j,n) -> Nat equals
:Def4:
(i + j) mod 2 to_power(n);
coherence;
end;
definition
let n;
let i be Nat;
assume A1: i is_expressible_by n;
func NEG_N(i,n) -> Nat equals
:Def5:
2 to_power(n) - i;
coherence
proof
i < 2 to_power(n) by A1,Def3;
then 2 to_power(n) - i > i - i by REAL_1:54;
then 2 to_power(n) - i > 0 by XCMPLX_1:14;
hence 2 to_power(n) - i is Nat by INT_1:16;
end;
end;
definition
let n;
let i be Nat;
func NEG_MOD(i,n) -> Nat equals
:Def6:
NEG_N(i,n) mod 2 to_power(n);
coherence;
end;
theorem Th12:
i is_expressible_by n implies ADD_MOD(i, NEG_MOD(i,n), n) = 0
proof
assume i is_expressible_by n;
then A1: i + NEG_N(i,n)
= i + (2 to_power(n) - i) by Def5
.= i + (2 to_power(n) + -i) by XCMPLX_0:def 8
.= i + -i + 2 to_power(n) by XCMPLX_1:1
.= 0 + 2 to_power(n) by XCMPLX_0:def 6;
thus ADD_MOD(i, NEG_MOD(i,n), n)
= (i + NEG_MOD(i,n)) mod 2 to_power(n) by Def4
.= (i + (NEG_N(i,n) mod 2 to_power(n)))
mod 2 to_power(n) by Def6
.= 2 to_power(n) mod 2 to_power(n) by A1,GR_CY_1:3
.= 0 by GR_CY_1:5;
end;
theorem Th13:
ADD_MOD(i,j,n) = ADD_MOD(j,i,n)
proof
thus ADD_MOD(i,j,n) = (i + j) mod 2 to_power(n) by Def4
.= ADD_MOD(j,i,n) by Def4;
end;
theorem Th14:
i is_expressible_by n implies ADD_MOD(0,i,n) = i
proof
assume i is_expressible_by n;
then A1:i < 2 to_power(n) by Def3;
thus ADD_MOD(0,i,n) = (0 + i) mod 2 to_power(n) by Def4
.= i by A1,GR_CY_1:4;
end;
theorem Th15:
ADD_MOD(ADD_MOD(i,j,n),k,n) = ADD_MOD(i,ADD_MOD(j,k,n),n)
proof
thus ADD_MOD(ADD_MOD(i,j,n),k,n)
= ADD_MOD((i+j) mod 2 to_power(n),k,n) by Def4
.= ((i+j) mod 2 to_power(n) + k) mod 2 to_power(n) by Def4
.= (i+j+k) mod 2 to_power(n) by GR_CY_1:3
.= (i+(j+k)) mod 2 to_power(n) by XCMPLX_1:1
.= (i + ((j+k) mod 2 to_power(n))) mod 2 to_power(n) by GR_CY_1:2
.= (i + ADD_MOD(j,k,n)) mod 2 to_power(n) by Def4
.= ADD_MOD(i,ADD_MOD(j,k,n),n) by Def4;
end;
theorem Th16:
ADD_MOD(i,j,n) is_expressible_by n
proof
A1: 2 to_power(n) > 0 by POWER:39;
ADD_MOD(i,j,n) = (i + j) mod 2 to_power(n) by Def4;
then ADD_MOD(i,j,n) < 2 to_power(n) by A1,NAT_1:46;
hence thesis by Def3;
end;
theorem
NEG_MOD(i,n) is_expressible_by n
proof
A1: 2 to_power(n) > 0 by POWER:39;
NEG_MOD(i,n) = NEG_N(i,n) mod 2 to_power(n) by Def6;
then NEG_MOD(i,n) < 2 to_power(n) by A1,NAT_1:46;
hence thesis by Def3;
end;
definition
let n, i be Nat;
func ChangeVal_1(i,n) -> Nat equals
:Def7:
2 to_power(n) if i = 0
otherwise i;
correctness;
end;
theorem Th18:
i is_expressible_by n implies
ChangeVal_1(i,n) <= 2 to_power(n) & ChangeVal_1(i,n) > 0
proof
assume A1: i is_expressible_by n;
A2: 2 to_power(n) > 0 by POWER:39;
per cases;
suppose i=0;
hence thesis by A2,Def7;
suppose A3: i<>0;
then ChangeVal_1(i,n) = i by Def7;
hence thesis by A1,A3,Def3,NAT_1:19;
end;
theorem Th19:
for n,a1,a2 be Nat holds a1 is_expressible_by n & a2 is_expressible_by n &
ChangeVal_1(a1,n) = ChangeVal_1(a2,n) implies a1 = a2
proof
let n;
let a1,a2 be Nat;
assume A1:a1 is_expressible_by n & a2 is_expressible_by n &
ChangeVal_1(a1,n) = ChangeVal_1(a2,n);
then A2: a1 <> 2 to_power(n) by Def3;
A3: a2 <> 2 to_power(n) by A1,Def3;
per cases;
suppose A4: ChangeVal_1(a1,n) = 2 to_power(n);
hence a2 = 0 by A1,A3,Def7
.= a1 by A2,A4,Def7;
suppose A5: ChangeVal_1(a1,n) <> 2 to_power(n);
then A6: a1 <> 0 by Def7;
a2 <> 0 by A1,A5,Def7;
hence a2 = ChangeVal_1(a1,n) by A1,Def7
.= a1 by A6,Def7;
end;
definition
let n;
let i be Nat;
func ChangeVal_2(i,n) -> Nat equals
:Def8:
0 if i = 2 to_power(n)
otherwise i;
correctness;
end;
theorem
i is_expressible_by n implies
ChangeVal_2(i,n) is_expressible_by n
proof
assume i is_expressible_by n;
then i < 2 to_power(n) by Def3;
then ChangeVal_2(i,n) < 2 to_power(n) by Def8;
hence thesis by Def3;
end;
theorem Th21:
for n,a1,a2 be Nat holds a1 <> 0 & a2 <> 0 &
ChangeVal_2(a1,n) = ChangeVal_2(a2,n) implies a1 = a2
proof
let n;
let a1,a2 be Nat;
assume A1: a1 <> 0 & a2 <> 0 & ChangeVal_2(a1,n) = ChangeVal_2(a2,n);
per cases;
suppose A2: ChangeVal_2(a1,n) = 0;
then a2 = 2 to_power(n) or a2 = 0 by A1,Def8;
hence a2 = a1 by A1,A2,Def8;
suppose A3: ChangeVal_2(a1,n) <> 0;
then A4:a1 <> 2 to_power(n) by Def8;
a2 <> 2 to_power(n) by A1,A3,Def8;
hence a2 = ChangeVal_2(a1,n) by A1,Def8
.= a1 by A4,Def8;
end;
definition
let n;
let i,j be Nat;
func MUL_MOD(i,j,n) -> Nat equals
:Def9:
ChangeVal_2((ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1),n);
coherence;
end;
definition
let n be non empty Nat;
let i be Nat;
assume A1: i is_expressible_by n & (2 to_power(n) + 1) is prime;
func INV_MOD(i,n) -> Nat means
:Def10:
MUL_MOD(i,it,n) = 1 & it is_expressible_by n;
existence
proof
A2: 2 to_power(n) > 0 by POWER:39;
2 to_power(n) + (1 - 1) > 0 by POWER:39;
then reconsider n2=2 to_power(n) + 1 - 1 as Nat by XCMPLX_1:29;
A3:2 to_power(n) + 1 > 0 + 1 by A2,REAL_1:53;
reconsider nn=2 to_power(n) + 1 as Nat;
n>0 by NAT_1:19;
then A4: 2 to_power(n) <> 1 by POWER:40;
2 to_power(n) + 1 >= 1 + 1 by A3,NAT_1:38;
then 2 to_power(n) + 1 - 1 >= 1 + 1 - 1 by REAL_1:49;
then 2 to_power(n) + 1 - 1 - 1 >= 1 + 1 - 1 - 1 by REAL_1:49;
then reconsider n3=2 to_power(n) + 1 - 1 - 1 as Nat by INT_1:16;
A5: n2 = 2 to_power(n) + (1 - 1) by XCMPLX_1:29
.= 2 to_power(n) + 0;
n2 * n2 = (2 to_power(n) + 1 - 1)*(2 to_power(n) + 1) -
(2 to_power(n) + 1 - 1)*1 by XCMPLX_1:40
.= (2 to_power(n) + 1)*(2 to_power(n) + 1 - 1) -
(2 to_power(n) + 1)*1 + 1 by XCMPLX_1:37
.= nn*n3 + 1 by XCMPLX_1:40;
then A6:(n2*n2) mod nn
= 1 mod nn by GR_CY_1:1
.= 1 by A3,GR_CY_1:4;
now per cases;
suppose A7: i=0;
consider j such that A8:j = 0;
take j;
A9: MUL_MOD(i,j,n)
= ChangeVal_2((ChangeVal_1(0,n)*ChangeVal_1(0,n)) mod nn,n)
by A7,A8,Def9
.= ChangeVal_2((2 to_power(n)*ChangeVal_1(0,n)) mod nn,n) by Def7
.= ChangeVal_2((n2*n2) mod nn,n) by A5,Def7
.= 1 by A4,A6,Def8;
j is_expressible_by n by A2,A8,Def3;
hence thesis by A9;
suppose A10: i<>0;
i < 2 to_power(n) by A1,Def3;
then i < 2 to_power(n)+1 by NAT_1:38;
then consider a being Nat such that
A11: (a*i) mod (2 to_power(n)+1) = 1 & a < (2 to_power(n)+1)
by A1,A3,A10,Th1;
A12: a <> 0 by A11,GR_CY_1:4;
take k=ChangeVal_2(a,n);
now per cases;
suppose A13:a <> 2 to_power(n);
then A14: k = a by Def8;
then k <= 2 to_power(n) by A11,NAT_1:38;
then k < 2 to_power(n) by A13,A14,REAL_1:def 5;
then A15: k is_expressible_by n by Def3;
MUL_MOD(i,k,n)
= ChangeVal_2((ChangeVal_1(i,n)*
ChangeVal_1(k,n)) mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((i*
ChangeVal_1(k,n)) mod (2 to_power(n)+1),n) by A10,Def7
.= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A12,A14,Def7
.= 1 by A4,A11,Def8;
hence thesis by A15;
suppose A16:a = 2 to_power(n);
then A17: k = 0 by Def8;
then A18: k is_expressible_by n by A2,Def3;
MUL_MOD(i,k,n)
= ChangeVal_2((ChangeVal_1(i,n)*
ChangeVal_1(k,n)) mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((i*
ChangeVal_1(k,n)) mod (2 to_power(n)+1),n) by A10,Def7
.= ChangeVal_2((i*a)mod (2 to_power(n)+1),n) by A16,A17,Def7
.= 1 by A4,A11,Def8;
hence thesis by A18;
end;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let a1, a2 be Nat such that
A19: MUL_MOD(i,a1,n) = 1 & a1 is_expressible_by n and
A20: MUL_MOD(i,a2,n) = 1 & a2 is_expressible_by n;
consider k being Nat such that
A21: k = ChangeVal_1(i,n);
A22: k <= 2 to_power(n) & k > 0 by A1,A21,Th18;
then A23: k < 2 to_power(n)+1 by NAT_1:38;
consider b1 being Nat such that
A24: b1 = ChangeVal_1(a1,n);
A25: b1 <= 2 to_power(n) & b1 > 0 by A19,A24,Th18;
then A26: b1 < 2 to_power(n)+1 by NAT_1:38;
consider b2 being Nat such that
A27: b2 = ChangeVal_1(a2,n);
A28: b2 <= 2 to_power(n) & b2 > 0 by A20,A27,Th18;
then A29: b2 < 2 to_power(n)+1 by NAT_1:38;
A30: (k * b1) mod (2 to_power(n)+1) <> 0 by A1,A22,A23,A25,A26,Th5;
A31:(k * b2) mod (2 to_power(n)+1) <> 0 by A1,A22,A23,A28,A29,Th5;
ChangeVal_2((k * b1) mod (2 to_power(n)+1),n)
= MUL_MOD(i,a2,n) by A19,A20,A21,A24,Def9
.= ChangeVal_2((k * b2) mod (2 to_power(n)+1),n) by A21,A27,Def9;
then A32: (k * b1) mod (2 to_power(n)+1)
= (k * b2) mod (2 to_power(n)+1) by A30,A31,Th21;
now per cases;
suppose A33:b1 <= b2;
then k*b1 <= k*b2 by NAT_1:20;
then consider t being Nat such that
A34: k*b2 - k*b1 = (2 to_power(n)+1)*t by A32,Th2;
consider b being Integer such that A35: b = b2 - b1;
b1 - b1 <= b2 - b1 by A33,REAL_1:49;
then 0 <= b2 - b1 by XCMPLX_1:14;
then reconsider b as Nat by A35,INT_1:16;
k*b = (2 to_power(n)+1)*t by A34,A35,XCMPLX_1:40;
then (2 to_power(n)+1) divides k*b by NAT_1:def 3;
then A36: (2 to_power(n)+1) divides k or (2 to_power(n)+1)
divides b
by A1,NAT_LAT:95;
A37: not ((2 to_power(n)+1) <= k) by A22,NAT_1:38;
b <= 2 to_power(n) by A28,A35,Th4;
then not ((2 to_power(n)+1) <= b) by NAT_1:38;
then A38:not(0 < b) by A22,A36,A37,NAT_1:54;
0 <= b by NAT_1:18;
then b2 - b1 + b1 = 0 + b1 by A35,A38,AXIOMS:21;
then b2 - (b1 - b1) = b1 by XCMPLX_1:37;
then b2 - 0 = b1 by XCMPLX_1:14;
hence b1 = b2;
suppose A39:b2 <= b1;
then k*b2 <= k*b1 by NAT_1:20;
then consider t being Nat such that
A40: k*b1 - k*b2 = (2 to_power(n)+1)*t by A32,Th2;
consider b being Integer such that A41: b = b1 - b2;
b2 - b2 <= b1 - b2 by A39,REAL_1:49;
then 0 <= b1 - b2 by XCMPLX_1:14;
then reconsider b as Nat by A41,INT_1:16;
k*b = (2 to_power(n)+1)*t by A40,A41,XCMPLX_1:40;
then (2 to_power(n)+1) divides k*b by NAT_1:def 3;
then A42: (2 to_power(n)+1) divides k or (2 to_power(n)+1)
divides b
by A1,NAT_LAT:95;
A43: not ((2 to_power(n)+1) <= k) by A22,NAT_1:38;
b <= 2 to_power(n) by A25,A41,Th4;
then not ((2 to_power(n)+1) <= b) by NAT_1:38;
then A44:not(0 < b) by A22,A42,A43,NAT_1:54;
0 <= b by NAT_1:18;
then b1 - b2 + b2 = 0 + b2 by A41,A44,AXIOMS:21;
then b1 - (b2 - b2) = b2 by XCMPLX_1:37;
then b1 - 0 = b2 by XCMPLX_1:14;
hence b2 = b1;
end;
hence thesis by A19,A20,A24,A27,Th19;
end;
end;
theorem Th22:
MUL_MOD(i,j,n) = MUL_MOD(j,i,n)
proof
MUL_MOD(i,j,n) = ChangeVal_2((ChangeVal_1(i,n)*ChangeVal_1(j,n))
mod (2 to_power(n)+1),n) by Def9
.= MUL_MOD(j,i,n) by Def9;
hence thesis;
end;
theorem Th23:
i is_expressible_by n implies MUL_MOD(1,i,n) = i
proof
assume i is_expressible_by n;
then A1:i < 2 to_power n by Def3;
A2:ChangeVal_1(1,n) = 1 by Def7;
A3:(1*ChangeVal_1(i,n)) mod ((2 to_power n)+1)
= (ChangeVal_1(i,n)) mod ((2 to_power n)+1);
per cases;
suppose A4:i = 0;
then A5:ChangeVal_1(i,n) = 2 to_power(n) by Def7;
2 to_power n < (2 to_power n)+1 by REAL_1:69;
then A6:(ChangeVal_1(i,n)) mod ((2 to_power n)+1) = 2 to_power(n)
by A5,GR_CY_1:4;
ChangeVal_2(2 to_power(n),n) = 0 by Def8;
hence thesis by A2,A3,A4,A6,Def9;
suppose i <> 0;
then A7:(ChangeVal_1(i,n)) mod ((2 to_power n)+1)
= i mod ((2 to_power n)+1) by Def7;
2 to_power n < (2 to_power n)+1 by REAL_1:69;
then i < (2 to_power n)+1 by A1,AXIOMS:22;
then A8:(ChangeVal_1(i,n)) mod ((2 to_power n)+1) = i by A7,GR_CY_1:4;
ChangeVal_2(i,n) = i by A1,Def8;
hence thesis by A2,A3,A8,Def9;
end;
theorem Th24:
(2 to_power(n)+1) is prime & i is_expressible_by n &
j is_expressible_by n & k is_expressible_by n implies
MUL_MOD(MUL_MOD(i,j,n),k,n) = MUL_MOD(i,MUL_MOD(j,k,n),n)
proof
assume A1:(2 to_power(n)+1) is prime & i is_expressible_by n &
j is_expressible_by n & k is_expressible_by n;
set I = ChangeVal_1(i,n);
set J = ChangeVal_1(j,n);
set K = ChangeVal_1(k,n);
I <= 2 to_power(n) & I > 0 by A1,Th18;
then A2:I < 2 to_power(n)+1 & I > 0 by NAT_1:38;
J <= 2 to_power(n) & J > 0 by A1,Th18;
then A3:J < 2 to_power(n)+1 & J > 0 by NAT_1:38;
K <= 2 to_power(n) & K > 0 by A1,Th18;
then A4:K < 2 to_power(n)+1 & K > 0 by NAT_1:38;
A5:MUL_MOD(i,j,n)
= ChangeVal_2((I*J) mod (2 to_power(n)+1),n) by Def9;
A6:MUL_MOD(j,k,n)
= ChangeVal_2((J*K) mod (2 to_power(n)+1),n) by Def9;
A7:2 to_power(n) < 2 to_power(n)+1 by REAL_1:69;
now
0 < 2 to_power(n) by POWER:39;
then 0 < (2 to_power(n)+1) by A7,AXIOMS:22;
then (I*J) mod (2 to_power(n)+1)
< (2 to_power(n)+1) by NAT_1:46;
then A8:(I*J) mod (2 to_power(n)+1)
<= 2 to_power(n) by NAT_1:38;
set CV = (I*J) mod (2 to_power(n)+1);
A9:CV <> 0 by A1,A2,A3,Th5;
now per cases by A8,AXIOMS:21;
suppose A10:CV = 2 to_power(n);
then MUL_MOD(i,j,n) = 0 by A5,Def8;
then A11:MUL_MOD(MUL_MOD(i,j,n),k,n)
= ChangeVal_2((ChangeVal_1(0,n)*K)
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A10,Def7
.= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n)
by EULER_2:10;
set CV2 = (J*K) mod (2 to_power(n)+1);
0 < 2 to_power(n) by POWER:39;
then 0 < (2 to_power(n)+1) by A7,AXIOMS:22;
then CV2 < (2 to_power(n)+1) by NAT_1:46;
then A12:CV2 <= 2 to_power(n) by NAT_1:38;
A13:CV2 <> 0 by A1,A3,A4,Th5;
now per cases by A12,AXIOMS:21;
suppose A14:CV2 = 2 to_power(n);
then MUL_MOD(i,MUL_MOD(j,k,n),n)
= MUL_MOD(i,0,n) by A6,Def8
.= ChangeVal_2((I*ChangeVal_1(0,n))
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A14,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n)
by EULER_2:10
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n)
by XCMPLX_1:4;
hence thesis by A11;
suppose A15:CV2 < 2 to_power(n);
MUL_MOD(j,k,n) = ChangeVal_2(CV2,n) by Def9
.= CV2 by A15,Def8;
then MUL_MOD(i,MUL_MOD(j,k,n),n)
= ChangeVal_2((I*ChangeVal_1(CV2,n))
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((I*CV2)
mod (2 to_power(n)+1),n) by A13,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n)
by EULER_2:10
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n)
by XCMPLX_1:4;
hence thesis by A11;
end;
hence thesis;
suppose CV < 2 to_power(n);
then MUL_MOD(i,j,n) = CV by A5,Def8;
then A16:MUL_MOD(MUL_MOD(i,j,n),k,n)
= ChangeVal_2((ChangeVal_1(CV,n)*K)
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((CV*K) mod (2 to_power(n)+1),n) by A9,Def7
.= ChangeVal_2(((I*J)*K) mod (2 to_power(n)+1),n)
by EULER_2:10;
set CV2 = (J*K) mod (2 to_power(n)+1);
0 < 2 to_power(n) by POWER:39;
then 0 < (2 to_power(n)+1) by A7,AXIOMS:22;
then CV2 < (2 to_power(n)+1) by NAT_1:46;
then A17:CV2 <= 2 to_power(n) by NAT_1:38;
A18:CV2 <> 0 by A1,A3,A4,Th5;
now per cases by A17,AXIOMS:21;
suppose A19:CV2 = 2 to_power(n);
then MUL_MOD(j,k,n) = 0 by A6,Def8;
then MUL_MOD(i,MUL_MOD(j,k,n),n)
= ChangeVal_2((I*ChangeVal_1(0,n))
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((I*CV2) mod (2 to_power(n)+1),n) by A19,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n)
by EULER_2:10
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n)
by XCMPLX_1:4;
hence thesis by A16;
suppose A20:CV2 < 2 to_power(n);
MUL_MOD(j,k,n) = ChangeVal_2(CV2,n) by Def9
.= CV2 by A20,Def8;
then MUL_MOD(i,MUL_MOD(j,k,n),n)
= ChangeVal_2((I*ChangeVal_1(CV2,n))
mod (2 to_power(n)+1),n) by Def9
.= ChangeVal_2((I*CV2)
mod (2 to_power(n)+1),n) by A18,Def7
.= ChangeVal_2((I*(J*K)) mod (2 to_power(n)+1),n)
by EULER_2:10
.= ChangeVal_2((I*J*K) mod (2 to_power(n)+1),n)
by XCMPLX_1:4;
hence thesis by A16;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th25:
MUL_MOD(i,j,n) is_expressible_by n
proof
A1:2 to_power n < (2 to_power n)+1 by REAL_1:69;
A2:0 < 2 to_power(n) by POWER:39;
then 0 < (2 to_power(n)+1) by A1,AXIOMS:22;
then (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1)
< (2 to_power(n)+1) by NAT_1:46;
then A3:(ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1)
<= 2 to_power(n) by NAT_1:38;
set CV = (ChangeVal_1(i,n)*ChangeVal_1(j,n)) mod (2 to_power(n)+1);
now per cases by A3,AXIOMS:21;
suppose CV = 2 to_power(n);
then ChangeVal_2(CV,n) = 0 by Def8;
then MUL_MOD(i,j,n) < 2 to_power(n) by A2,Def9;
hence thesis by Def3;
suppose A4:CV < 2 to_power(n);
then ChangeVal_2(CV,n) = CV by Def8;
then MUL_MOD(i,j,n) = CV by Def9;
hence thesis by A4,Def3;
end;
hence thesis;
end;
theorem
ChangeVal_2(i,n) = 1 implies i = 1
proof
assume A1:ChangeVal_2(i,n) = 1;
assume A2:i <> 1;
now per cases;
suppose i = 2 to_power(n);
hence contradiction by A1,Def8;
suppose i <> 2 to_power(n);
hence contradiction by A1,A2,Def8;
end;
hence thesis;
end;
begin :: Operations of IDEA Cryptograms
:: We define three IDEA's operations IDEAoperationA, IDEAoperationB
:: and IDEAoperationC using the basic operators. IDEA Cryptogram
:: encrypts 64-bit plain text to 64-bit ciphertext. These texts
:: are divided into 4 16-bits text blocks. Here, we use m as the
:: text block sequence. And, IDEA's operations use key sequence
:: explains k in this section. n is bit-length of text blocks.
:: Definiton of IDEA Operation A
definition
let n;
let m,k be FinSequence of NAT;
func IDEAoperationA(m, k, n) -> FinSequence of NAT means
:Def11:
len(it) = len(m) &
for i being Nat st i in dom m holds
(i=1 implies it.i = MUL_MOD(m.1, k.1, n)) &
(i=2 implies it.i = ADD_MOD(m.2, k.2, n)) &
(i=3 implies it.i = ADD_MOD(m.3, k.3, n)) &
(i=4 implies it.i = MUL_MOD(m.4, k.4, n)) &
(i<>1 & i <> 2 & i<>3 & i<>4 implies it.i = m.i);
existence
proof
defpred P[set,set] means
($1=1 implies $2 = MUL_MOD(m.1, k.1, n)) &
($1=2 implies $2 = ADD_MOD(m.2, k.2, n)) &
($1=3 implies $2 = ADD_MOD(m.3, k.3, n)) &
($1=4 implies $2 = MUL_MOD(m.4, k.4, n)) &
($1<>1 & $1 <> 2 & $1<>3 & $1<>4 implies $2 = m.$1);
A1: for j st j in Seg len m ex x being Element of NAT st
P[j,x]
proof
let j be Nat such that j in Seg len m;
per cases;
suppose A2: j = 1;
take MUL_MOD(m.1, k.1, n);
thus thesis by A2;
suppose A3: j = 2;
take ADD_MOD(m.2, k.2, n);
thus thesis by A3;
suppose A4: j = 3;
take ADD_MOD(m.3, k.3, n);
thus thesis by A4;
suppose A5: j = 4;
take MUL_MOD(m.4, k.4, n);
thus thesis by A5;
suppose A6: j<>1 & j<>2 & j<>3 & j<>4;
take m.j;
thus thesis by A6;
end;
A7:dom m = Seg len m by FINSEQ_1:def 3;
consider z being FinSequence of NAT such that
A8: dom z = Seg len m and
A9: for i st i in Seg len m holds P[i,z.i] from SeqDEx(A1);
take z;
thus thesis by A7,A8,A9,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A10: len(z1) = len(m) &
for i being Nat st i in dom m holds
(i=1 implies z1.i = MUL_MOD(m.1, k.1, n)) &
(i=2 implies z1.i = ADD_MOD(m.2, k.2, n)) &
(i=3 implies z1.i = ADD_MOD(m.3, k.3, n)) &
(i=4 implies z1.i = MUL_MOD(m.4, k.4, n)) &
(i<>1 & i <> 2 & i<>3 & i<>4 implies z1.i = m.i) and
A11: len(z2) = len(m) &
for i st i in dom m holds
(i=1 implies z2.i = MUL_MOD(m.1, k.1, n)) &
(i=2 implies z2.i = ADD_MOD(m.2, k.2, n)) &
(i=3 implies z2.i = ADD_MOD(m.3, k.3, n)) &
(i=4 implies z2.i = MUL_MOD(m.4, k.4, n)) &
(i<>1 & i <> 2 & i<>3 & i<>4 implies z2.i = m.i);
A12:dom m = Seg len z1 by A10,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
A13:dom m = Seg len z2 by A11,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
now let j be Nat;
assume A14: j in dom m;
now per cases;
suppose A15: j = 1;
hence z1.j = MUL_MOD(m.1, k.1, n) by A10,A14
.= z2.j by A11,A14,A15;
suppose A16: j = 2;
hence z1.j = ADD_MOD(m.2, k.2, n) by A10,A14
.= z2.j by A11,A14,A16;
suppose A17: j = 3;
hence z1.j = ADD_MOD(m.3, k.3, n) by A10,A14
.= z2.j by A11,A14,A17;
suppose A18: j = 4;
hence z1.j = MUL_MOD(m.4, k.4, n) by A10,A14
.= z2.j by A11,A14,A18;
suppose A19: j<>1 & j<>2 & j<>3 & j<>4;
hence z1.j = m.j by A10,A14
.= z2.j by A11,A14,A19;
end;
hence z1.j = z2.j;
end;
hence z1 = z2 by A12,A13,FINSEQ_1:17;
end;
end;
:: Definiton of IDEA Operation B
reserve m,k,k1,k2 for FinSequence of NAT;
definition
let n be non empty Nat;
let m,k be FinSequence of NAT;
func IDEAoperationB(m, k, n) -> FinSequence of NAT means
:Def12:
len(it) = len(m) & for i being Nat st i in dom m holds
(i=1 implies it.i =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=2 implies it.i =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i=3 implies it.i =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=4 implies it.i =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i<>1 & i <> 2 & i<>3 & i<>4 implies it.i = m.i);
existence
proof
defpred P[set,set] means
($1=1 implies $2 =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
($1=2 implies $2 =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
($1=3 implies $2 =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
($1=4 implies $2 =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
($1<>1 & $1 <> 2 & $1<>3 & $1<>4 implies $2 = m.$1);
A1: for j st j in Seg len m ex x being Element of NAT st P[j,x]
proof
let j be Nat such that j in Seg len m;
per cases;
suppose A2: j = 1;
take Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n)));
thus thesis by A2;
suppose A3: j = 2;
take Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n)));
thus thesis by A3;
suppose A4: j = 3;
take Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n)));
thus thesis by A4;
suppose A5: j = 4;
take Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n)));
thus thesis by A5;
suppose A6: j<>1 & j<>2 & j<>3 & j<>4;
take m.j;
thus thesis by A6;
end;
consider z being FinSequence of NAT such that
A7: dom z = Seg len m and
A8: for i st i in Seg len m holds P[i,z.i] from SeqDEx(A1);
A9:Seg len m = dom m by FINSEQ_1:def 3;
take z;
thus thesis by A7,A8,A9,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A10: len(z1) = len(m) &
for i st i in dom m holds
(i=1 implies z1.i =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=2 implies z1.i =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i=3 implies z1.i =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=4 implies z1.i =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i<>1 & i <> 2 & i<>3 & i<>4 implies z1.i = m.i) and
A11: len(z2) = len(m) &
for i st i in dom m holds
(i=1 implies z2.i =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=2 implies z2.i =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i=3 implies z2.i =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))))&
(i=4 implies z2.i =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))))&
(i<>1 & i <> 2 & i<>3 & i<>4 implies z2.i = m.i);
A12: dom m = Seg len(z1) by A10,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
A13: dom m = Seg len(z2) by A11,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
now let j be Nat;
assume A14: j in dom m;
now per cases;
suppose A15: j = 1;
hence z1.j =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))) by A10,A14
.= z2.j by A11,A14,A15;
suppose A16: j = 2;
hence z1.j =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))) by A10,A14
.= z2.j by A11,A14,A16;
suppose A17: j = 3;
hence z1.j =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))) by A10,A14
.= z2.j by A11,A14,A17;
suppose A18: j = 4;
hence z1.j =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))) by A10,A14
.= z2.j by A11,A14,A18;
suppose A19: j<>1 & j<>2 & j<>3 & j<>4;
hence z1.j = m.j by A10,A14
.= z2.j by A11,A14,A19;
end;
hence z1.j = z2.j;
end;
hence z1 = z2 by A12,A13,FINSEQ_1:17;
end;
end;
:: Definiton of IDEA Operation C
definition
let m be FinSequence of NAT;
func IDEAoperationC(m) -> FinSequence of NAT means
:Def13:
len(it) = len(m) &
for i being Nat st i in dom m holds
it.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i));
existence
proof
defpred P[set,set] means
($1=2 implies $2 = m.3) & ($1=3 implies $2 = m.2) &
($1<>2 & $1<>3 implies $2 = m.$1);
A1: for k be Nat st k in Seg len m ex x being Element of NAT st P[k,x]
proof
let k be Nat such that
k in Seg len m;
per cases;
suppose A2: k = 2;
take m.3;
thus thesis by A2;
suppose A3: k = 3;
take m.2;
thus thesis by A3;
suppose A4: k<>2 & k<>3;
take m.k;
thus thesis by A4;
end;
consider z being FinSequence of NAT such that
A5: dom z = Seg len m and
A6: for i st i in Seg len m holds P[i,z.i] from SeqDEx(A1);
A7:for i st i in Seg len m holds IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i
proof
let i be Nat;
assume A8:i in Seg len m;
A9:i = 2 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.3 by CQC_LANG:def
1;
A10:i = 3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.2
proof
assume A11:i = 3;
then IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i)
by CQC_LANG:def 1
.= m.2 by A11,CQC_LANG:def 1;
hence thesis;
end;
i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = m.i
proof
assume A12:i <> 2 & i <> 3;
then IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = IFEQ(i,3,m.2,m.i)
by CQC_LANG:def 1
.= m.i by A12,CQC_LANG:def 1;
hence thesis;
end;
then i<>2 & i<>3 implies IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) = z.i
by A6,A8;
hence thesis by A6,A8,A9,A10;
end;
A13:Seg len m = dom m by FINSEQ_1:def 3;
take z;
thus thesis by A5,A7,A13,FINSEQ_1:def 3;
end;
uniqueness
proof
let z1,z2 be FinSequence of NAT such that
A14:len(z1) = len(m) &
for i st i in dom m holds
z1.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) and
A15:len(z2) = len(m) &
for i st i in dom m holds
z2.i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i));
A16: dom m = Seg len(z1) by A14,FINSEQ_1:def 3
.= dom z1 by FINSEQ_1:def 3;
A17: dom m = Seg len(z2) by A15,FINSEQ_1:def 3
.= dom z2 by FINSEQ_1:def 3;
now let j be Nat;
assume A18: j in dom m;
now per cases;
suppose j = 2;
then A19:IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.3 by CQC_LANG:def 1;
then z2.j = m.3 by A15,A18;
hence z1.j = z2.j by A14,A18,A19;
suppose A20: j = 3;
A21:j = 3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.2
proof
assume A22:j = 3;
then IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j)
by CQC_LANG:def 1
.= m.2 by A22,CQC_LANG:def 1;
hence thesis;
end;
then z2.j = m.2 by A15,A18,A20;
hence z1.j = z2.j by A14,A18,A20,A21;
suppose A23: j<>2 & j<>3;
A24:j<>2 & j<>3 implies IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = m.j
proof
assume A25:j <> 2 & j <> 3;
then IFEQ(j,2,m.3,IFEQ(j,3,m.2,m.j)) = IFEQ(j,3,m.2,m.j)
by CQC_LANG:def 1
.= m.j by A25,CQC_LANG:def 1
;
hence thesis;
end;
then z2.j = m.j by A15,A18,A23;
hence z1.j = z2.j by A14,A18,A23,A24;
end;
hence z1.j = z2.j;
end;
hence z1 = z2 by A16,A17,FINSEQ_1:17;
end;
end;
theorem Th27:
len m >= 4 implies
IDEAoperationA(m,k,n).1 is_expressible_by n &
IDEAoperationA(m,k,n).2 is_expressible_by n &
IDEAoperationA(m,k,n).3 is_expressible_by n &
IDEAoperationA(m,k,n).4 is_expressible_by n
proof
assume A1: len m >= 4;
then 1 <= len m by AXIOMS:22;
then 1 in Seg len m by FINSEQ_1:3;
then 1 in dom m by FINSEQ_1:def 3;
then A2: IDEAoperationA(m,k,n).1 = MUL_MOD(m.1, k.1, n) by Def11;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then A3: IDEAoperationA(m,k,n).2 = ADD_MOD(m.2, k.2, n) by Def11;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then A4: IDEAoperationA(m,k,n).3 = ADD_MOD(m.3, k.3, n) by Def11;
4 in Seg len m by A1,FINSEQ_1:3;
then 4 in dom m by FINSEQ_1:def 3;
then IDEAoperationA(m,k,n).4 = MUL_MOD(m.4, k.4, n) by Def11;
hence thesis by A2,A3,A4,Th16,Th25;
end;
theorem Th28:
for n being non empty Nat holds
len m >= 4 implies
IDEAoperationB(m,k,n).1 is_expressible_by n &
IDEAoperationB(m,k,n).2 is_expressible_by n &
IDEAoperationB(m,k,n).3 is_expressible_by n &
IDEAoperationB(m,k,n).4 is_expressible_by n
proof
let n be non empty Nat;
assume A1: len m >= 4;
then 1 <= len m by AXIOMS:22;
then 1 in Seg len m by FINSEQ_1:3;
then 1 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).1 =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))) by Def12;
then A2: IDEAoperationB(m,k,n).1 < 2 to_power n by BINARI_3:1;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).2 =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))) by Def12;
then A3: IDEAoperationB(m,k,n).2 < 2 to_power n by BINARI_3:1;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).3 =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence
MUL_MOD(ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n))) by Def12;
then A4: IDEAoperationB(m,k,n).3 < 2 to_power n by BINARI_3:1;
4 in Seg len m by A1,FINSEQ_1:3;
then 4 in dom m by FINSEQ_1:def 3;
then IDEAoperationB(m,k,n).4 =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence
ADD_MOD(MUL_MOD(Absval((n-BinarySequence m.1) 'xor'
(n-BinarySequence m.3)),k.5,n),MUL_MOD(ADD_MOD(MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),
k.5,n),Absval((n-BinarySequence m.2) 'xor'
(n-BinarySequence m.4)),n),k.6,n),n))) by Def12;
then IDEAoperationB(m,k,n).4 < 2 to_power n by BINARI_3:1;
hence thesis by A2,A3,A4,Def3;
end;
Lm3:
for i st i = 2 & i in dom m holds IDEAoperationC(m).i = m.3
proof
let i be Nat;
assume A1:i = 2 & i in dom m;
then IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by Def13
.= m.3 by A1,CQC_LANG:def 1;
hence thesis;
end;
Lm4:
for i st i = 3 & i in dom m holds IDEAoperationC(m).i = m.2
proof
let i be Nat;
assume A1:i = 3 & i in dom m;
then IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by Def13
.= IFEQ(i,3,m.2,m.i) by A1,CQC_LANG:def 1
.= m.2 by A1,CQC_LANG:def 1;
hence thesis;
end;
Lm5:
for i st i <> 2 & i <> 3 & i in dom m holds IDEAoperationC(m).i = m.i
proof
let i be Nat;
assume A1:i <> 2 & i <> 3 & i in dom m;
then IDEAoperationC(m).i = IFEQ(i,2,m.3,IFEQ(i,3,m.2,m.i)) by Def13
.= IFEQ(i,3,m.2,m.i) by A1,CQC_LANG:def 1
.= m.i by A1,CQC_LANG:def 1;
hence thesis;
end;
theorem
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n implies
IDEAoperationC(m).1 is_expressible_by n &
IDEAoperationC(m).2 is_expressible_by n &
IDEAoperationC(m).3 is_expressible_by n &
IDEAoperationC(m).4 is_expressible_by n
proof
assume that A1: len m >= 4 and
A2: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n;
1 <= len m by A1,AXIOMS:22;
then 1 in Seg len m by FINSEQ_1:3;
then A3:1 in dom m by FINSEQ_1:def 3;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then A4: 2 in dom m by FINSEQ_1:def 3;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then A5: 3 in dom m by FINSEQ_1:def 3;
4 in Seg len m by A1,FINSEQ_1:3;
then 4 in dom m by FINSEQ_1:def 3;
hence thesis by A2,A3,A4,A5,Lm3,Lm4,Lm5;
end;
theorem Th30:
for n being non empty Nat,m,k1,k2 holds
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k2.1=INV_MOD(k1.1,n) & k2.2=NEG_MOD(k1.2,n) &
k2.3=NEG_MOD(k1.3,n) & k2.4=INV_MOD(k1.4,n) implies
IDEAoperationA( IDEAoperationA(m,k1,n), k2, n) = m
proof
let n be non empty Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: 2 to_power(n)+1 is prime &
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n and
A2: k2.1=INV_MOD(k1.1,n) and
A3: k2.2=NEG_MOD(k1.2,n) and
A4: k2.3=NEG_MOD(k1.3,n) and
A5: k2.4=INV_MOD(k1.4,n);
A6:k2.1 is_expressible_by n by A1,A2,Def10;
A7:k2.4 is_expressible_by n by A1,A5,Def10;
consider I1 being FinSequence of NAT such that
A8: I1 = IDEAoperationA(m,k1,n);
consider I2 being FinSequence of NAT such that
A9: I2 = IDEAoperationA(I1,k2,n);
A10: Seg len m = dom m by FINSEQ_1:def 3;
A11: Seg len m = Seg len(I1) by A8,Def11
.= Seg len(I2) by A9,Def11
.= dom I2 by FINSEQ_1:def 3;
Seg len m = dom m by FINSEQ_1:def 3;
then A12:4 in dom m by A1,FINSEQ_1:3;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then A13:3 in dom m by FINSEQ_1:def 3;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then A14:2 in dom m by FINSEQ_1:def 3;
1 <= len m by A1,AXIOMS:22;
then 1 in Seg len m by FINSEQ_1:3;
then A15:1 in dom m by FINSEQ_1:def 3;
now let j be Nat;
assume A16:j in Seg len m;
then j in Seg len I1 by A8,Def11;
then A17:j in dom I1 by FINSEQ_1:def 3;
A18:j in dom m by A16,FINSEQ_1:def 3;
now per cases;
suppose A19: j = 1;
hence I2.j = MUL_MOD(I1.1, k2.1, n) by A9,A17,Def11
.= MUL_MOD(MUL_MOD(m.1, k1.1, n),k2.1,n)
by A8,A15,Def11
.= MUL_MOD(m.1, MUL_MOD(k1.1,k2.1,n), n) by A1,A6,Th24
.= MUL_MOD(m.1, 1, n) by A1,A2,Def10
.= MUL_MOD(1, m.1, n) by Th22
.= m.j by A1,A19,Th23;
suppose A20: j = 2;
hence I2.j = ADD_MOD(I1.2, k2.2, n) by A9,A17,Def11
.= ADD_MOD(ADD_MOD(m.2, k1.2, n), k2.2, n)
by A8,A14,Def11
.= ADD_MOD(m.2, ADD_MOD(k1.2, k2.2, n), n) by Th15
.= ADD_MOD(m.2, 0, n) by A1,A3,Th12
.= ADD_MOD(0, m.2, n) by Th13
.= m.j by A1,A20,Th14;
suppose A21: j = 3;
hence I2.j = ADD_MOD(I1.3, k2.3, n) by A9,A17,Def11
.= ADD_MOD(ADD_MOD(m.3, k1.3, n), k2.3, n)
by A8,A13,Def11
.= ADD_MOD(m.3, ADD_MOD(k1.3, k2.3, n), n) by Th15
.= ADD_MOD(m.3, 0, n) by A1,A4,Th12
.= ADD_MOD(0, m.3, n) by Th13
.= m.j by A1,A21,Th14;
suppose A22: j = 4;
hence I2.j = MUL_MOD(I1.4, k2.4, n) by A9,A17,Def11
.= MUL_MOD(MUL_MOD(m.4, k1.4, n),k2.4,n)
by A8,A12,Def11
.= MUL_MOD(m.4, MUL_MOD(k1.4,k2.4,n), n) by A1,A7,Th24
.= MUL_MOD(m.4, 1, n) by A1,A5,Def10
.= MUL_MOD(1, m.4, n) by Th22
.= m.j by A1,A22,Th23;
suppose A23: j<>1 & j<>2 & j<>3 & j<>4;
hence I2.j = I1.j by A9,A17,Def11
.= m.j by A8,A18,A23,Def11;
end;
hence I2.j = m.j;
end;
hence thesis by A8,A9,A10,A11,FINSEQ_1:17;
end;
theorem Th31:
for n being non empty Nat,m,k1,k2 holds
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k2.1=INV_MOD(k1.1,n) & k2.2=NEG_MOD(k1.3,n) &
k2.3=NEG_MOD(k1.2,n) & k2.4=INV_MOD(k1.4,n) implies
IDEAoperationA(IDEAoperationC(IDEAoperationA(IDEAoperationC(m),k1,n)),k2,n)
= m
proof
let n be non empty Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: 2 to_power(n)+1 is prime &
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n and
A2: k2.1=INV_MOD(k1.1,n) and
A3: k2.2=NEG_MOD(k1.3,n) and
A4: k2.3=NEG_MOD(k1.2,n) and
A5: k2.4=INV_MOD(k1.4,n);
A6:k2.1 is_expressible_by n by A1,A2,Def10;
A7:k2.4 is_expressible_by n by A1,A5,Def10;
consider I1 being FinSequence of NAT such that
A8: I1 = IDEAoperationC(m);
consider I2 being FinSequence of NAT such that
A9: I2 = IDEAoperationA(I1,k1,n);
A10: len(I2) = len(I1) &
for i being Nat st i in dom I1 holds
(i=1 implies I2.i = MUL_MOD(I1.1, k1.1, n)) &
(i=2 implies I2.i = ADD_MOD(I1.2, k1.2, n)) &
(i=3 implies I2.i = ADD_MOD(I1.3, k1.3, n)) &
(i=4 implies I2.i = MUL_MOD(I1.4, k1.4, n)) &
(i<>1 & i <> 2 & i<>3 & i<>4 implies I2.i = I1.i)by A9,Def11;
consider I3 being FinSequence of NAT such that
A11: I3 = IDEAoperationC(I2);
A12: len(I3) = len(I2) &
for i being Nat st i in dom I2 holds
(i=2 implies I3.i = I2.3) &
(i=3 implies I3.i = I2.2) &
(i<>2 & i <> 3 implies I3.i = I2.i) by A11,Def13,Lm3,Lm4,Lm5;
consider I4 being FinSequence of NAT such that
A13: I4 = IDEAoperationA(I3,k2,n);
A14: len(I4) = len(I3) &
for i being Nat st i in dom I3 holds
(i=1 implies I4.i = MUL_MOD(I3.1, k2.1, n)) &
(i=2 implies I4.i = ADD_MOD(I3.2, k2.2, n)) &
(i=3 implies I4.i = ADD_MOD(I3.3, k2.3, n)) &
(i=4 implies I4.i = MUL_MOD(I3.4, k2.4, n)) &
(i<>1 & i <> 2 & i<>3 & i<>4 implies I4.i = I3.i)by A13,Def11;
A15: Seg len m = dom m by FINSEQ_1:def 3;
A16: Seg len m = Seg len(I1) by A8,Def13
.= Seg len(I2) by A9,Def11
.= Seg len(I3) by A11,Def13
.= Seg len(I4) by A13,Def11
.= dom I4 by FINSEQ_1:def 3;
1 <= len m by A1,AXIOMS:22;
then A17: 1 in Seg len m by FINSEQ_1:3;
then 1 in Seg len(I1) & 1 in Seg len(I2) &
1 in Seg len(I3) & 1 in Seg len(I4)
by A8,A10,A12,A14,Def13;
then A18: 1 in dom(I1) & 1 in dom(I2) &
1 in dom(I3) & 1 in dom(I4) by FINSEQ_1:def 3;
A19:1 in dom m by A17,FINSEQ_1:def 3;
2 <= len m by A1,AXIOMS:22;
then A20: 2 in Seg len m by FINSEQ_1:3;
then 2 in Seg len(I1) & 2 in Seg len(I2) &
2 in Seg len(I3) & 2 in Seg len(I4)
by A8,A10,A12,A14,Def13;
then A21: 2 in dom(I1) & 2 in dom(I2) &
2 in dom(I3) & 2 in dom(I4) by FINSEQ_1:def 3;
A22:2 in dom m by A20,FINSEQ_1:def 3;
3 <= len m by A1,AXIOMS:22;
then A23: 3 in Seg len m by FINSEQ_1:3;
then 3 in Seg len(I1) & 3 in Seg len(I2) &
3 in Seg len(I3) & 3 in Seg len(I4)
by A8,A10,A12,A14,Def13;
then A24: 3 in dom(I1) & 3 in dom(I2) &
3 in dom(I3) & 3 in dom(I4) by FINSEQ_1:def 3;
A25:3 in dom m by A23,FINSEQ_1:def 3;
A26: 4 in Seg len m by A1,FINSEQ_1:3;
then 4 in Seg len(I1) & 4 in Seg len(I2) &
4 in Seg len(I3) & 4 in Seg len(I4)
by A8,A10,A12,A14,Def13;
then A27: 4 in dom(I1) & 4 in dom(I2) &
4 in dom(I3) & 4 in dom(I4) by FINSEQ_1:def 3;
A28:4 in dom m by A26,FINSEQ_1:def 3;
now let j be Nat;
assume A29:j in Seg len m;
then A30: j in Seg len I1 by A8,Def13;
then A31: j in Seg len I2 by A9,Def11;
then A32: j in Seg len I3 by A11,Def13;
A33: j in dom I1 by A30,FINSEQ_1:def 3;
A34: j in dom I2 by A31,FINSEQ_1:def 3;
A35: j in dom I3 by A32,FINSEQ_1:def 3;
A36:j in dom m by A29,FINSEQ_1:def 3;
now per cases;
suppose A37: j = 1;
hence I4.j = MUL_MOD(I3.1, k2.1, n) by A13,A18,Def11
.= MUL_MOD(I2.1, k2.1, n) by A11,A18,Lm5
.= MUL_MOD(MUL_MOD(I1.1, k1.1, n), k2.1, n)
by A9,A18,Def11
.= MUL_MOD(MUL_MOD(m.1, k1.1, n), k2.1, n)
by A8,A19,Lm5
.= MUL_MOD(m.1, MUL_MOD(k1.1, k2.1, n), n) by A1,A6,Th24
.= MUL_MOD(m.1, 1, n) by A1,A2,Def10
.= MUL_MOD(1, m.1, n) by Th22
.= m.j by A1,A37,Th23;
suppose A38: j = 2;
hence I4.j = ADD_MOD(I3.2, k2.2, n) by A13,A21,Def11
.= ADD_MOD(I2.3, k2.2, n) by A11,A21,Lm3
.= ADD_MOD(ADD_MOD(I1.3, k1.3, n), k2.2, n)
by A9,A24,Def11
.= ADD_MOD(ADD_MOD(m.2, k1.3, n), k2.2, n)
by A8,A25,Lm4
.= ADD_MOD(m.2, ADD_MOD(k1.3, k2.2, n), n) by Th15
.= ADD_MOD(m.2, 0, n) by A1,A3,Th12
.= ADD_MOD(0, m.2, n) by Th13
.= m.j by A1,A38,Th14;
suppose A39: j = 3;
hence I4.j = ADD_MOD(I3.3, k2.3, n) by A13,A24,Def11
.= ADD_MOD(I2.2, k2.3, n) by A11,A24,Lm4
.= ADD_MOD(ADD_MOD(I1.2, k1.2, n), k2.3, n)
by A9,A21,Def11
.= ADD_MOD(ADD_MOD(m.3, k1.2, n), k2.3, n)
by A8,A22,Lm3
.= ADD_MOD(m.3, ADD_MOD(k1.2, k2.3, n), n) by Th15
.= ADD_MOD(m.3, 0, n) by A1,A4,Th12
.= ADD_MOD(0, m.3, n) by Th13
.= m.j by A1,A39,Th14;
suppose A40: j = 4;
hence I4.j = MUL_MOD(I3.4, k2.4, n) by A13,A27,Def11
.= MUL_MOD(I2.4, k2.4, n) by A11,A27,Lm5
.= MUL_MOD(MUL_MOD(I1.4, k1.4, n), k2.4, n)
by A9,A27,Def11
.= MUL_MOD(MUL_MOD(m.4, k1.4, n), k2.4, n)
by A8,A28,Lm5
.= MUL_MOD(m.4, MUL_MOD(k1.4, k2.4, n), n) by A1,A7,Th24
.= MUL_MOD(m.4, 1, n) by A1,A5,Def10
.= MUL_MOD(1, m.4, n) by Th22
.= m.j by A1,A40,Th23;
suppose A41: j<>1 & j<>2 & j<>3 & j<>4;
hence I4.j = I3.j by A13,A35,Def11
.= I2.j by A11,A34,A41,Lm5
.= I1.j by A9,A33,A41,Def11
.= m.j by A8,A36,A41,Lm5;
end;
hence I4.j = m.j;
end;
hence thesis by A8,A9,A11,A13,A15,A16,FINSEQ_1:17;
end;
theorem Th32:
for n being non empty Nat,m,k1,k2 holds
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n &
k2.5=k1.5 & k2.6=k1.6 implies
IDEAoperationB( IDEAoperationB(m,k1,n), k2, n) = m
proof
let n be non empty Nat;
let m,k1,k2 be FinSequence of NAT;
assume that
A1: 2 to_power(n)+1 is prime &
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n and
A2: k2.5= k1.5 and
A3: k2.6= k1.6;
consider t10 being Nat such that
A4:t10 = MUL_MOD(
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence m.3)),k1.5,n);
consider t11 being Nat such that
A5:t11 = MUL_MOD(ADD_MOD(t10,
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence m.4)),n),k1.6,n);
consider t12 being Nat such that
A6:t12 = ADD_MOD(t10, t11, n);
consider I1 being FinSequence of NAT such that
A7: I1 = IDEAoperationB(m,k1,n);
consider t20 being Nat such that
A8:t20 = MUL_MOD(
Absval((n-BinarySequence I1.1) 'xor' (n-BinarySequence I1.3)),k2.5,n);
consider t21 being Nat such that
A9:t21 = MUL_MOD(ADD_MOD(t20,
Absval((n-BinarySequence I1.2) 'xor' (n-BinarySequence I1.4)),n),k2.6,n);
consider I2 being FinSequence of NAT such that
A10: I2 = IDEAoperationB(I1,k2,n);
A11: Seg len m = dom m by FINSEQ_1:def 3;
A12: Seg len m = Seg len(I1) by A7,Def12
.= Seg len(I2) by A10,Def12
.= dom I2 by FINSEQ_1:def 3;
4 in Seg len m by A1,FINSEQ_1:3;
then 4 in dom m by FINSEQ_1:def 3;
then A13:I1.4 =
Absval((n-BinarySequence m.4) 'xor' (n-BinarySequence t12))
by A4,A5,A6,A7,Def12;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then A14:I1.3 =
Absval((n-BinarySequence m.3) 'xor' (n-BinarySequence t11))
by A4,A5,A7,Def12;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then A15:I1.2 =
Absval((n-BinarySequence m.2) 'xor' (n-BinarySequence t12))
by A4,A5,A6,A7,Def12;
1 <= len m by A1,AXIOMS:22;
then 1 in Seg len m by FINSEQ_1:3;
then 1 in dom m by FINSEQ_1:def 3;
then A16:I1.1 =
Absval((n-BinarySequence m.1) 'xor' (n-BinarySequence t11))
by A4,A5,A7,Def12;
then A17: t20
= MUL_MOD(
Absval(((n-BinarySequence m.1) 'xor'
(n-BinarySequence t11)) 'xor'
(n-BinarySequence Absval((n-BinarySequence m.3) 'xor'
(n-BinarySequence t11)))),k2.5,n) by A8,A14,BINARI_3:37
.= MUL_MOD(
Absval(((n-BinarySequence m.1) 'xor'
(n-BinarySequence t11)) 'xor'
((n-BinarySequence m.3) 'xor'
(n-BinarySequence t11))),k2.5,n) by BINARI_3:37
.= MUL_MOD(
Absval((n-BinarySequence m.1) 'xor'
((n-BinarySequence t11) 'xor'
((n-BinarySequence t11) 'xor'
(n-BinarySequence m.3)))),k2.5,n) by Th10
.= MUL_MOD(
Absval((n-BinarySequence m.1) 'xor'
(((n-BinarySequence t11) 'xor'
(n-BinarySequence t11)) 'xor'
(n-BinarySequence m.3))),k2.5,n) by Th10
.= MUL_MOD(
Absval((n-BinarySequence m.1) 'xor'
(ZERO(n) 'xor'
(n-BinarySequence m.3))),k2.5,n) by Th7
.= t10 by A2,A4,Th9;
then A18: t21
= MUL_MOD(ADD_MOD(t10,
Absval(((n-BinarySequence m.2) 'xor' (n-BinarySequence t12)
) 'xor'
(n-BinarySequence Absval(
(n-BinarySequence m.4) 'xor' (n-BinarySequence t12)
)
)
),n),k2.6,n) by A9,A13,A15,BINARI_3:37
.= MUL_MOD(ADD_MOD(t10,
Absval(((n-BinarySequence m.2) 'xor' (n-BinarySequence t12)
) 'xor'
((n-BinarySequence m.4) 'xor' (n-BinarySequence t12)
)
),n),k2.6,n) by BINARI_3:37
.= MUL_MOD(ADD_MOD(t10,
Absval( (n-BinarySequence m.2) 'xor'
((n-BinarySequence t12) 'xor'
((n-BinarySequence t12) 'xor' (n-BinarySequence m.4))
)
),n),k2.6,n) by Th10
.= MUL_MOD(ADD_MOD(t10,
Absval( (n-BinarySequence m.2) 'xor'
((n-BinarySequence t12) 'xor'
(n-BinarySequence t12) 'xor' (n-BinarySequence m.4)
)
),n),k2.6,n) by Th10
.= MUL_MOD(ADD_MOD(t10,
Absval( (n-BinarySequence m.2) 'xor'
(ZERO(n) 'xor' (n-BinarySequence m.4)
)
),n),k2.6,n) by Th7
.= t11 by A3,A5,Th9;
now let j be Nat;
assume A19:j in Seg len m;
then j in Seg len I1 by A7,Def12;
then A20: j in dom I1 by FINSEQ_1:def 3;
A21:j in dom m by A19,FINSEQ_1:def 3;
now per cases;
suppose A22: j = 1;
A23: m.1 < 2 to_power n by A1,Def3;
thus I2.j
= Absval((n-BinarySequence I1.1) 'xor' (n-BinarySequence t11)) by A8,A9,A10
,A18,A20,A22,Def12
.= Absval(((n-BinarySequence m.1) 'xor' (n-BinarySequence t11)) 'xor'
(n-BinarySequence t11)) by A16,BINARI_3:37
.= Absval((n-BinarySequence m.1) 'xor' ((n-BinarySequence t11) 'xor'
(n-BinarySequence t11))) by Th10
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.1)) by Th7
.= Absval(n-BinarySequence m.1) by Th9
.= m.j by A22,A23,BINARI_3:36;
suppose A24: j = 2;
A25: m.2 < 2 to_power n by A1,Def3;
thus
I2.j
= Absval((n-BinarySequence I1.2) 'xor' (n-BinarySequence t12))
by A6,A8,A9,A10,A17,A18,A20
,A24,Def12
.= Absval(((n-BinarySequence m.2) 'xor' (n-BinarySequence t12)) 'xor'
(n-BinarySequence t12)) by A15,BINARI_3:37
.= Absval((n-BinarySequence m.2) 'xor' ((n-BinarySequence t12) 'xor'
(n-BinarySequence t12)))by Th10
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.2)) by Th7
.= Absval(n-BinarySequence m.2) by Th9
.= m.j by A24,A25,BINARI_3:36;
suppose A26: j = 3;
A27: m.3 < 2 to_power n by A1,Def3;
thus I2.j
= Absval((n-BinarySequence I1.3) 'xor' (n-BinarySequence t11)) by A8,A9,A10
,A18,A20,A26,Def12
.= Absval(((n-BinarySequence m.3) 'xor' (n-BinarySequence t11)) 'xor'
(n-BinarySequence t11)) by A14,BINARI_3:37
.= Absval((n-BinarySequence m.3) 'xor' ((n-BinarySequence t11) 'xor'
(n-BinarySequence t11))) by Th10
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.3)) by Th7
.= Absval(n-BinarySequence m.3) by Th9
.= m.j by A26,A27,BINARI_3:36;
suppose A28: j = 4;
A29: m.4 < 2 to_power n by A1,Def3;
thus
I2.j
= Absval((n-BinarySequence I1.4) 'xor' (n-BinarySequence t12))
by A6,A8,A9,A10,A17,A18,
A20,A28,Def12
.= Absval(((n-BinarySequence m.4) 'xor' (n-BinarySequence t12)) 'xor'
(n-BinarySequence t12)) by A13,BINARI_3:37
.= Absval((n-BinarySequence m.4) 'xor' ((n-BinarySequence t12) 'xor'
(n-BinarySequence t12))) by Th10
.= Absval(ZERO(n) 'xor' (n-BinarySequence m.4)) by Th7
.= Absval(n-BinarySequence m.4) by Th9
.= m.j by A28,A29,BINARI_3:36;
suppose A30: j<>1 & j<>2 & j<>3 & j<>4;
hence I2.j = I1.j by A10,A20,Def12
.= m.j by A7,A21,A30,Def12;
end;
hence I2.j = m.j;
end;
hence thesis by A7,A10,A11,A12,FINSEQ_1:17;
end;
theorem
for m holds len m >= 4 implies IDEAoperationC( IDEAoperationC(m) ) = m
proof
let m be FinSequence of NAT;
assume A1: len m >= 4;
consider I1 being FinSequence of NAT such that
A2: I1 = IDEAoperationC(m);
consider I2 being FinSequence of NAT such that
A3: I2 = IDEAoperationC(I1);
A4: Seg len m = dom m by FINSEQ_1:def 3;
A5: Seg len m = Seg len(I1) by A2,Def13
.= Seg len(I2) by A3,Def13
.= dom I2 by FINSEQ_1:def 3;
3 <= len m by A1,AXIOMS:22;
then 3 in Seg len m by FINSEQ_1:3;
then 3 in dom m by FINSEQ_1:def 3;
then A6:I1.3 = m.2 by A2,Lm4;
2 <= len m by A1,AXIOMS:22;
then 2 in Seg len m by FINSEQ_1:3;
then 2 in dom m by FINSEQ_1:def 3;
then A7:I1.2 = m.3 by A2,Lm3;
now let j be Nat;
assume A8:j in Seg len m;
then j in Seg len I1 by A2,Def13;
then A9:j in dom I1 by FINSEQ_1:def 3;
A10:j in dom m by A8,FINSEQ_1:def 3;
now per cases;
suppose j = 2;
hence I2.j = m.j by A3,A6,A9,Lm3;
suppose j = 3;
hence I2.j = m.j by A3,A7,A9,Lm4;
suppose A11: j<>2 & j<>3;
hence I2.j = I1.j by A3,A9,Lm5
.= m.j by A2,A10,A11,Lm5;
end;
hence I2.j = m.j;
end;
hence thesis by A2,A3,A4,A5,FINSEQ_1:17;
end;
begin :: Sequences of IDEA Cryptogram's operations
:: For making a model of IDEA, we define sequences of IDEA's
:: operations IDEA_P, IDEA_PS, IDEA_PE, IDEA_Q, IDEA_QS and
:: IDEA_QE. And, we define MESSAGES as plain and cipher text.
definition
func MESSAGES -> set equals
:Def14:
NAT*;
coherence;
end;
definition
cluster MESSAGES -> non empty;
coherence by Def14;
end;
definition
cluster -> Function-like Relation-like Element of MESSAGES;
coherence by Def14,FINSEQ_1:def 11;
end;
definition
cluster -> FinSequence-like Element of MESSAGES;
coherence by Def14,FINSEQ_1:def 11;
end;
definition
let n be non empty Nat,k;
func IDEA_P(k,n) -> Function of MESSAGES, MESSAGES means
:Def15:
for m holds it.m = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationA(IDEAoperationC(
IDEAoperationB(F,k,n)),k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationA(IDEAoperationC(
IDEAoperationB(F,k,n)),k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationA(IDEAoperationC(
IDEAoperationB(F,k,n)),k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationA(IDEAoperationC(
IDEAoperationB(m,k,n)),k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationA(IDEAoperationC(
IDEAoperationB(m,k,n)),k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(IDEAoperationC(
IDEAoperationB(jj,k,n)),k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition
let n be non empty Nat,k;
func IDEA_Q(k,n) -> Function of MESSAGES, MESSAGES means
:Def16:
for m holds it.m = IDEAoperationB(IDEAoperationA(IDEAoperationC(m),k,n),k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationB(IDEAoperationA(
IDEAoperationC(F),k,n),k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationB(IDEAoperationA(
IDEAoperationC(F),k,n),k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationB(IDEAoperationA(
IDEAoperationC(F),k,n),k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationB(IDEAoperationA(
IDEAoperationC(m),k,n),k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationB(IDEAoperationA(
IDEAoperationC(m),k,n),k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationB(IDEAoperationA(
IDEAoperationC(jj),k,n),k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition
let r,lk be Nat,n be non empty Nat,Key be Matrix of lk,6,NAT;
func IDEA_P_F(Key,n,r) -> FinSequence means
:Def17:
len it = r & for i st i in dom it holds it.i = IDEA_P(Line(Key,i),n);
existence
proof
deffunc F(Nat)=IDEA_P(Line(Key,$1),n);
consider z being FinSequence such that
A1: len z = r and
A2: for k being Nat st k in Seg r holds
z.k= F(k) from SeqLambda;
A3:Seg r = dom z by A1,FINSEQ_1:def 3;
take z;
thus thesis by A1,A2,A3;
end;
uniqueness
proof
let z1,z2 be FinSequence such that
A4: len z1 = r &
for i being Nat st i in dom z1 holds
z1.i = IDEA_P(Line(Key,i),n) and
A5: len z2 = r &
for i being Nat st i in dom z2 holds
z2.i = IDEA_P(Line(Key,i),n);
A6: Seg r = dom z1 by A4,FINSEQ_1:def 3;
A7: Seg r = dom z2 by A5,FINSEQ_1:def 3;
now let j be Nat;
assume A8: j in Seg r;
then A9:j in dom z2 by A5,FINSEQ_1:def 3;
j in dom z1 by A4,A8,FINSEQ_1:def 3;
then z1.j = IDEA_P(Line(Key,j),n) by A4
.= z2.j by A5,A9;
hence z1.j = z2.j;
end;
hence z1 = z2 by A6,A7,FINSEQ_1:17;
end;
end;
definition
let r,lk be Nat,n be non empty Nat,Key be Matrix of lk,6,NAT;
cluster IDEA_P_F(Key,n,r) -> Function-yielding;
coherence
proof
for x being set st x in dom IDEA_P_F(Key,n,r) holds
IDEA_P_F(Key,n,r).x is Function
proof
let x be set;
assume A1: x in dom IDEA_P_F(Key,n,r);
then consider xx being Nat such that A2: xx = x;
IDEA_P_F(Key,n,r).xx = IDEA_P(Line(Key,xx),n) by A1,A2,Def17;
hence IDEA_P_F(Key,n,r).x is Function by A2;
end;
hence IDEA_P_F(Key,n,r) is Function-yielding by PRALG_1:def 15;
end;
end;
definition
let r,lk be Nat,n be non empty Nat,Key be Matrix of lk,6,NAT;
func IDEA_Q_F(Key,n,r) -> FinSequence means
:Def18:
len it = r & for i st i in dom it holds it.i = IDEA_Q(Line(Key,r-'i+1),n);
existence
proof
deffunc F(Nat)=IDEA_Q(Line(Key,r-'$1+1),n);
consider z being FinSequence such that
A1: len z = r and
A2: for k being Nat st k in Seg r holds
z.k= F(k) from SeqLambda;
A3:Seg r = dom z by A1,FINSEQ_1:def 3;
take z;
thus thesis by A1,A2,A3;
end;
uniqueness
proof
let z1,z2 be FinSequence such that
A4: len z1 = r &
for i being Nat st i in dom z1 holds
z1.i = IDEA_Q(Line(Key,r-'i+1),n) and
A5: len z2 = r &
for i being Nat st i in dom z2 holds
z2.i = IDEA_Q(Line(Key,r-'i+1),n);
A6: Seg r = dom z1 by A4,FINSEQ_1:def 3;
A7: Seg r = dom z2 by A5,FINSEQ_1:def 3;
now let j be Nat;
assume A8: j in Seg r;
then A9:j in dom z2 by A5,FINSEQ_1:def 3;
j in dom z1 by A4,A8,FINSEQ_1:def 3;
then z1.j = IDEA_Q(Line(Key,r-'j+1),n) by A4
.= z2.j by A5,A9;
hence z1.j = z2.j;
end;
hence z1 = z2 by A6,A7,FINSEQ_1:17;
end;
end;
definition
let r,lk be Nat,n be non empty Nat,Key be Matrix of lk,6,NAT;
cluster IDEA_Q_F(Key,n,r) -> Function-yielding;
coherence
proof
for x being set st x in dom IDEA_Q_F(Key,n,r) holds
IDEA_Q_F(Key,n,r).x is Function
proof
let x be set;
assume A1: x in dom IDEA_Q_F(Key,n,r);
then consider xx being Nat such that A2: xx = x;
IDEA_Q_F(Key,n,r).xx = IDEA_Q(Line(Key,r-'xx+1),n) by A1,A2,Def18;
hence IDEA_Q_F(Key,n,r).x is Function by A2;
end;
hence IDEA_Q_F(Key,n,r) is Function-yielding by PRALG_1:def 15;
end;
end;
definition
let k,n;
func IDEA_PS(k,n) -> Function of MESSAGES, MESSAGES means
:Def19:
for m holds it.m = IDEAoperationA(m,k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationA(F,k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationA(m,k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationA(m,k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(jj,k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition
let k,n;
func IDEA_QS(k,n) -> Function of MESSAGES, MESSAGES means
:Def20:
for m holds it.m = IDEAoperationA(m,k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationA(F,k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationA(F,k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationA(F,k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationA(m,k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationA(m,k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(jj,k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition
let n be non empty Nat,k;
func IDEA_PE(k,n) -> Function of MESSAGES, MESSAGES means
:Def21:
for m holds it.m = IDEAoperationA(IDEAoperationB(m,k,n),k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationA(IDEAoperationB(F,k,n),k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationA(
IDEAoperationB(F,k,n),k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationA(
IDEAoperationB(F,k,n),k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationA(
IDEAoperationB(m,k,n),k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationA(
IDEAoperationB(m,k,n),k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationA(
IDEAoperationB(jj,k,n),k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
definition
let n be non empty Nat,k;
func IDEA_QE(k,n) -> Function of MESSAGES, MESSAGES means
:Def22:
for m holds it.m = IDEAoperationB(IDEAoperationA(m,k,n),k,n);
existence
proof
defpred P[set,set] means
ex F be FinSequence of NAT st
$1 = F & $2 = IDEAoperationB(IDEAoperationA(F,k,n),k,n);
A1: for e being Element of MESSAGES
ex u being Element of MESSAGES st P[e,u]
proof
let e be Element of MESSAGES;
reconsider F = e as FinSequence of NAT by Def14,FINSEQ_1:def 11;
reconsider u = IDEAoperationB(
IDEAoperationA(F,k,n),k,n) as Element of MESSAGES
by Def14,FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider m1 being Function of MESSAGES,MESSAGES such that
A2: for e being Element of MESSAGES holds P[e,m1.e]
from FuncExD(A1);
take m1;
let m be FinSequence of NAT;
m is Element of MESSAGES by Def14,FINSEQ_1:def 11;
then consider F being FinSequence of NAT such that
A3: m = F & m1.m = IDEAoperationB(
IDEAoperationA(F,k,n),k,n) by A2;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of MESSAGES, MESSAGES such that
A4: for m being FinSequence of NAT holds
m1.m = IDEAoperationB(
IDEAoperationA(m,k,n),k,n) and
A5: for m being FinSequence of NAT holds
m2.m = IDEAoperationB(
IDEAoperationA(m,k,n),k,n);
m1 = m2
proof
A6: dom m1 = MESSAGES & dom m2 = MESSAGES by FUNCT_2:def 1;
now
let j be set;
assume A7: j in MESSAGES;
consider jj being set such that A8: jj = j;
reconsider jj as FinSequence of NAT
by A7,A8,Def14,FINSEQ_1:def 11;
thus m1.j = IDEAoperationB(
IDEAoperationA(jj,k,n),k,n) by A4,A8
.= m2.j by A5,A8;
end;
hence m1 = m2 by A6,FUNCT_1:9;
end;
hence thesis;
end;
end;
theorem Th34:
for n being non empty Nat,m,k1,k2
holds 2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n &
k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.3,n) &
k2.3 = NEG_MOD(k1.2,n) & k2.4 = INV_MOD(k1.4,n) &
k2.5 = k1.5 & k2.6 = k1.6 implies
(IDEA_Q(k2,n)*IDEA_P(k1,n)).m = m
proof
let n be non empty Nat;
let m,k1,k2;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n and
A4: k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n and
A5: k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.3,n) &
k2.3 = NEG_MOD(k1.2,n) & k2.4 = INV_MOD(k1.4,n) and
A6: k2.5 = k1.5 & k2.6 = k1.6;
dom IDEA_P(k1,n) = MESSAGES & dom IDEA_Q(k2,n) = MESSAGES
by FUNCT_2:def 1;
then A7: m in dom IDEA_P(k1,n) & m in dom IDEA_Q(k2,n)
by Def14,FINSEQ_1:def 11;
A8: len IDEAoperationB(m,k1,n) >= 4 by A2,Def12;
A9: IDEAoperationB(m,k1,n).1 is_expressible_by n &
IDEAoperationB(m,k1,n).2 is_expressible_by n &
IDEAoperationB(m,k1,n).3 is_expressible_by n &
IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th28;
(IDEA_Q(k2,n)*IDEA_P(k1,n)).m
= IDEA_Q(k2,n).(IDEA_P(k1,n).m) by A7,FUNCT_1:23
.= IDEA_Q(k2,n).
IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k1,n)),k1,n)
by Def15
.= IDEAoperationB(IDEAoperationA(IDEAoperationC(
IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k1,n)),k1,n)
),k2,n),k2,n)
by Def16
.= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n)
by A1,A4,A5,A8,A9,Th31
.= m by A1,A2,A3,A4,A6,Th32;
hence (IDEA_Q(k2,n)*IDEA_P(k1,n)).m = m;
end;
theorem Th35:
for n being non empty Nat,m,k1,k2 holds
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) &
k2.3 = NEG_MOD(k1.3,n) & k2.4 = INV_MOD(k1.4,n) implies
(IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = m
proof
let n be non empty Nat;
let m,k1,k2;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n and
A4: k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n and
A5: k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) &
k2.3 = NEG_MOD(k1.3,n) & k2.4 = INV_MOD(k1.4,n);
dom IDEA_PS(k1,n) = MESSAGES & dom IDEA_QS(k2,n) = MESSAGES
by FUNCT_2:def 1;
then m in dom IDEA_PS(k1,n) & m in dom IDEA_QS(k2,n)
by Def14,FINSEQ_1:def 11;
then (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m
= IDEA_QS(k2,n).(IDEA_PS(k1,n).m) by FUNCT_1:23
.= IDEA_QS(k2,n).IDEAoperationA(m,k1,n) by Def19
.= IDEAoperationA(IDEAoperationA(m,k1,n),k2,n) by Def20
.= m by A1,A2,A3,A4,A5,Th30;
hence (IDEA_QS(k2,n)*IDEA_PS(k1,n)).m = m;
end;
theorem Th36:
for n being non empty Nat,m,k1,k2 holds
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n &
k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) &
k2.3 = NEG_MOD(k1.3,n) & k2.4 = INV_MOD(k1.4,n) &
k2.5 = k1.5 & k2.6 = k1.6 implies
(IDEA_QE(k2,n)*IDEA_PE(k1,n)).m = m
proof
let n be non empty Nat;
let m,k1,k2;
assume that
A1: 2 to_power(n)+1 is prime and
A2: len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n and
A4: k1.1 is_expressible_by n & k1.2 is_expressible_by n &
k1.3 is_expressible_by n & k1.4 is_expressible_by n &
k1.5 is_expressible_by n & k1.6 is_expressible_by n and
A5: k2.1 = INV_MOD(k1.1,n) & k2.2 = NEG_MOD(k1.2,n) &
k2.3 = NEG_MOD(k1.3,n) & k2.4 = INV_MOD(k1.4,n) and
A6: k2.5 = k1.5 & k2.6 = k1.6;
dom IDEA_PE(k1,n) = MESSAGES & dom IDEA_QE(k2,n) = MESSAGES
by FUNCT_2:def 1;
then A7: m in dom IDEA_PE(k1,n) & m in dom IDEA_QE(k2,n)
by Def14,FINSEQ_1:def 11;
A8: len IDEAoperationB(m,k1,n) >= 4 by A2,Def12;
A9: IDEAoperationB(m,k1,n).1 is_expressible_by n &
IDEAoperationB(m,k1,n).2 is_expressible_by n &
IDEAoperationB(m,k1,n).3 is_expressible_by n &
IDEAoperationB(m,k1,n).4 is_expressible_by n by A2,Th28;
(IDEA_QE(k2,n)*IDEA_PE(k1,n)).m
= IDEA_QE(k2,n).(IDEA_PE(k1,n).m) by A7,FUNCT_1:23
.= IDEA_QE(k2,n).
IDEAoperationA(IDEAoperationB(m,k1,n),k1,n) by Def21
.= IDEAoperationB(IDEAoperationA(
IDEAoperationA(IDEAoperationB(m,k1,n),k1,n),k2,n),k2,n)
by Def22
.= IDEAoperationB(IDEAoperationB(m,k1,n),k2,n)
by A1,A4,A5,A8,A9,Th30
.= m by A1,A2,A3,A4,A6,Th32;
hence (IDEA_QE(k2,n)*IDEA_PE(k1,n)).m = m;
end;
theorem Th37:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds IDEA_P_F(Key,n,(k+1)) =
IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>
proof
let n be non empty Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>)
= len IDEA_P_F(Key,n,k) +
len <* IDEA_P(Line(Key,(k+1)),n) *> by FINSEQ_1:35
.= k + len <* IDEA_P(Line(Key,(k+1)),n) *> by Def17
.= k + 1 by FINSEQ_1:56;
then A1: len IDEA_P_F(Key,n,(k+1))
= len (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>) by Def17;
for i being Nat st 1 <= i & i <= len IDEA_P_F(Key,n,(k+1))
holds IDEA_P_F(Key,n,(k+1)).i =
(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i
proof
let i be Nat;
assume A2: 1 <= i & i <= len IDEA_P_F(Key,n,(k+1));
then A3: 1 <= i & i <= k+1 by Def17;
i in Seg len IDEA_P_F(Key,n,(k+1)) by A2,FINSEQ_1:3;
then A4:i in dom IDEA_P_F(Key,n,(k+1)) by FINSEQ_1:def 3;
dom <* IDEA_P(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
then A5: 1 in dom <*IDEA_P(Line(Key,(k+1)),n)*> by FINSEQ_1:3;
now per cases;
suppose i <> k+1;
then 1 <= i & i <= k by A3,NAT_1:26;
then i in Seg k by FINSEQ_1:3;
then i in Seg len IDEA_P_F(Key,n,k) by Def17;
then A6:i in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
hence (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i
= IDEA_P_F(Key,n,k).i by FINSEQ_1:def 7
.= IDEA_P(Line(Key,i),n) by A6,Def17
.= IDEA_P_F(Key,n,(k+1)).i by A4,Def17;
suppose A7: i = k+1;
hence (IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).i
=(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>).
(len IDEA_P_F(Key,n,k) + 1) by Def17
.= <* IDEA_P(Line(Key,(k+1)),n) *>.1 by A5,FINSEQ_1:def 7
.= IDEA_P(Line(Key,(k+1)),n) by FINSEQ_1:57
.= IDEA_P_F(Key,n,(k+1)).i by A4,A7,Def17;
end;
hence thesis;
end;
hence thesis by A1,FINSEQ_1:18;
end;
theorem Th38:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds IDEA_Q_F(Key,n,(k+1)) =
<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)
proof
let n be non empty Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k))
= len <* IDEA_Q(Line(Key,k+1),n) *> +
len IDEA_Q_F(Key,n,k) by FINSEQ_1:35
.= len <* IDEA_Q(Line(Key,k+1),n) *> + k by Def18
.= k + 1 by FINSEQ_1:56;
then A1: len IDEA_Q_F(Key,n,(k+1))
= len (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k))
by Def18;
for i being Nat st 1 <= i & i <= len IDEA_Q_F(Key,n,(k+1))
holds IDEA_Q_F(Key,n,(k+1)).i =
(<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i
proof
let i be Nat;
assume A2: 1 <= i & i <= len IDEA_Q_F(Key,n,(k+1));
then A3: 1 <= i & i <= k+1 by Def18;
i in Seg len IDEA_Q_F(Key,n,(k+1)) by A2,FINSEQ_1:3;
then A4:i in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
dom <* IDEA_Q(Line(Key,(k+1)),n) *> = Seg 1 by FINSEQ_1:def 8;
then A5: 1 in dom <*IDEA_Q(Line(Key,(k+1)),n)*> by FINSEQ_1:3;
A6: 1 <= k+1 by A3,AXIOMS:22;
1 <= len IDEA_Q_F(Key,n,(k+1)) by A2,AXIOMS:22;
then 1 in Seg len IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:3;
then A7:1 in dom IDEA_Q_F(Key,n,(k+1)) by FINSEQ_1:def 3;
now per cases;
suppose A8: i <> 1;
consider ii be Integer such that A9: ii = i - 1;
A10: ii + 1 = i - (1 - 1) by A9,XCMPLX_1:37
.= i;
1 - 1 <= i - 1 by A2,REAL_1:49;
then reconsider ii as Nat by A9,INT_1:16;
1 < i by A2,A8,REAL_1:def 5;
then 1 + 1 <= i by NAT_1:38;
then A11: 1 + 1 - 1 <= i - 1 by REAL_1:49;
i-1 <= k+1-1 by A3,REAL_1:49;
then A12:i-1 <= k+(1-1) by XCMPLX_1:29;
then ii in Seg k by A9,A11,FINSEQ_1:3;
then ii in Seg len IDEA_Q_F(Key,n,k) by Def18;
then A13: ii in dom IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
ii - ii <= k - ii by A9,A12,REAL_1:49;
then A14: 0 <= k - ii by XCMPLX_1:14;
(k+1) - i >= i - i by A3,REAL_1:49;
then A15: (k+1) - i >= 0 by XCMPLX_1:14;
A16: k -' ii = k - (i - 1) by A9,A14,BINARITH:def 3
.= k - i + 1 by XCMPLX_1:37
.= k + -i + 1 by XCMPLX_0:def 8
.= (k+1) + -i by XCMPLX_1:1
.= (k+1) - i by XCMPLX_0:def 8
.=(k+1) -' i by A15,BINARITH:def 3;
thus (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i
=(<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).
(len <*IDEA_Q(Line(Key,(k+1)),n)*>+ii)
by A10,FINSEQ_1:57
.=IDEA_Q_F(Key,n,k).ii by A13,FINSEQ_1:def 7
.=IDEA_Q(Line(Key,(k+1)-'i+1),n) by A13,A16,Def18
.=IDEA_Q_F(Key,n,k+1).i by A4,Def18;
suppose A17: i = 1;
hence (<* IDEA_Q(Line(Key,k+1),n) *>^IDEA_Q_F(Key,n,k)).i
= <* IDEA_Q(Line(Key,k+1),n) *>.1 by A5,FINSEQ_1:def 7
.= IDEA_Q(Line(Key,k+1),n) by FINSEQ_1:57
.= IDEA_Q(Line(Key,(k+1)-'1 + 1),n) by A6,AMI_5:4
.= IDEA_Q_F(Key,n,k+1).i by A7,A17,Def18;
end;
hence thesis;
end;
hence thesis by A1,FINSEQ_1:18;
end;
theorem Th39:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds IDEA_P_F(Key,n,k) is FuncSeq-like FinSequence
proof
let n be non empty Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
deffunc F(set)=MESSAGES;
consider p being FinSequence such that A1: len p = k+1 and
A2: for j being Nat st j in Seg(k+1) holds p.j = F(j) from SeqLambda;
A3: len p = len IDEA_P_F(Key,n,k)+1 by A1,Def17;
for i being Nat st i in dom IDEA_P_F(Key,n,k)
holds IDEA_P_F(Key,n,k).i in Funcs(p.i, p.(i+1))
proof
let i be Nat;
assume A4: i in dom IDEA_P_F(Key,n,k);
then i in Seg len IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
then i in Seg k by Def17;
then 1 <= i & i <= k by FINSEQ_1:3;
then 1 <= i & i <= k+1 & 1 <= (i+1) & (i+1) <=
k+1 by AXIOMS:24,NAT_1:37;
then i in Seg (k+1) & (i+1) in Seg (k+1) by FINSEQ_1:3;
then A5: p.i = MESSAGES & p.(i+1) = MESSAGES by A2;
IDEA_P_F(Key,n,k).i = IDEA_P(Line(Key,i),n) by A4,Def17;
hence IDEA_P_F(Key,n,k).i in Funcs(p.i,p.(i+1)) by A5,FUNCT_2:12;
end;
hence thesis by A3,FUNCT_7:def 8;
end;
theorem Th40:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds IDEA_Q_F(Key,n,k) is FuncSeq-like FinSequence
proof
let n be non empty Nat;
let lk be Nat;
let Key be Matrix of lk,6,NAT;
let k be Nat;
deffunc F(set)=MESSAGES;
consider p being FinSequence such that A1: len p = k+1 and
A2: for j being Nat st j in Seg(k+1) holds p.j = F(j) from SeqLambda;
A3: len p = len IDEA_Q_F(Key,n,k)+1 by A1,Def18;
for i being Nat st i in dom IDEA_Q_F(Key,n,k)
holds IDEA_Q_F(Key,n,k).i in Funcs(p.i, p.(i+1))
proof
let i be Nat;
assume A4: i in dom IDEA_Q_F(Key,n,k);
then i in Seg len IDEA_Q_F(Key,n,k) by FINSEQ_1:def 3;
then i in Seg k by Def18;
then 1 <= i & i <= k by FINSEQ_1:3;
then 1 <= i & i <= k+1 & 1 <= (i+1) & (i+1) <=
k+1 by AXIOMS:24,NAT_1:37;
then i in Seg (k+1) & (i+1) in Seg (k+1) by FINSEQ_1:3;
then A5: p.i = MESSAGES & p.(i+1) = MESSAGES by A2;
IDEA_Q_F(Key,n,k).i = IDEA_Q(Line(Key,k-'i+1),n) by A4,Def18;
hence IDEA_Q_F(Key,n,k).i in Funcs(p.i,p.(i+1)) by A5,FUNCT_2:12;
end;
hence thesis by A3,FUNCT_7:def 8;
end;
theorem Th41:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds k <> 0 implies
IDEA_P_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
let n be non empty Nat;
let lk be Nat,
Key be Matrix of lk,6,NAT,
k be Nat;
assume A1: k<>0;
A2: IDEA_P_F(Key,n,k) is FuncSequence by Th39;
A3: lastrng IDEA_P_F(Key,n,k) c= MESSAGES
proof
0 < k by A1,NAT_1:19;
then 0+1 < k+1 by REAL_1:53;
then A4:1 <= k & k <= k by NAT_1:38;
k = len IDEA_P_F(Key,n,k) by Def17;
then k in Seg len IDEA_P_F(Key,n,k) by A4,FINSEQ_1:3;
then A5:k in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,k)) <> 0 by A1,Def17;
then not(IDEA_P_F(Key,n,k)=<*>MESSAGES)
by FINSEQ_1:32;
then lastrng IDEA_P_F(Key,n,k)
= proj2 (IDEA_P_F(Key,n,k).
len (IDEA_P_F(Key,n,k))) by FUNCT_7:def 7
.= proj2 (IDEA_P_F(Key,n,k).k) by Def17
.= proj2 (IDEA_P(Line(Key,k),n)) by A5,Def17
.= rng IDEA_P(Line(Key,k),n) by FUNCT_5:21;
hence lastrng IDEA_P_F(Key,n,k) c= MESSAGES by RELSET_1:12;
end;
firstdom IDEA_P_F(Key,n,k) = MESSAGES
proof
0 < k by A1,NAT_1:19;
then 0+1 < k+1 by REAL_1:53;
then A6:1 <= 1 & 1 <= k by NAT_1:38;
k = len IDEA_P_F(Key,n,k) by Def17;
then 1 in Seg len IDEA_P_F(Key,n,k) by A6,FINSEQ_1:3;
then A7:1 in dom IDEA_P_F(Key,n,k) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,k)) = k by Def17;
then not(IDEA_P_F(Key,n,k)=<*>MESSAGES) by A1,FINSEQ_1:32;
hence firstdom IDEA_P_F(Key,n,k)
= proj1 (IDEA_P_F(Key,n,k).1) by FUNCT_7:def 6
.= proj1 (IDEA_P(Line(Key,1),n)) by A7,Def17
.= dom IDEA_P(Line(Key,1),n) by FUNCT_5:21
.= MESSAGES by FUNCT_2:def 1;
end;
hence thesis by A2,A3,FUNCT_7:def 9;
end;
theorem Th42:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
k being Nat holds k <> 0 implies
IDEA_Q_F(Key,n,k) is FuncSequence of MESSAGES,MESSAGES
proof
let n be non empty Nat,
lk be Nat,
Key be Matrix of lk,6,NAT,
r be Nat;
assume A1: r<>0;
A2: IDEA_Q_F(Key,n,r) is FuncSequence by Th40;
A3: lastrng IDEA_Q_F(Key,n,r) c= MESSAGES
proof
0 < r by A1,NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A4:1 <= r & r <= r by NAT_1:38;
r = len IDEA_Q_F(Key,n,r) by Def18;
then r in Seg len IDEA_Q_F(Key,n,r) by A4,FINSEQ_1:3;
then A5:r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
then not(IDEA_Q_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
then lastrng IDEA_Q_F(Key,n,r)
= proj2 (IDEA_Q_F(Key,n,r).
len (IDEA_Q_F(Key,n,r)))
by FUNCT_7:def 7
.= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
.= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A5,Def18
.= rng IDEA_Q(Line(Key,r-'r+1),n) by FUNCT_5:21;
hence lastrng IDEA_Q_F(Key,n,r) c= MESSAGES by RELSET_1:12;
end;
firstdom IDEA_Q_F(Key,n,r) = MESSAGES
proof
0 < r by A1,NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A6:1 <= 1 & 1 <= r by NAT_1:38;
r = len IDEA_Q_F(Key,n,r) by Def18;
then 1 in Seg len IDEA_Q_F(Key,n,r) by A6,FINSEQ_1:3;
then A7:1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A1,Def18;
then not(IDEA_Q_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
hence firstdom IDEA_Q_F(Key,n,r)
= proj1 (IDEA_Q_F(Key,n,r).1) by FUNCT_7:def 6
.= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A7,Def18
.= dom IDEA_Q(Line(Key,r-'1+1),n) by FUNCT_5:21
.= MESSAGES by FUNCT_2:def 1;
end;
hence thesis by A2,A3,FUNCT_7:def 9;
end;
theorem Th43:
for n being non empty Nat,M being FinSequence of NAT,m,k st
M = IDEA_P(k,n).m & len m >= 4 holds len M >= 4 &
M.1 is_expressible_by n & M.2 is_expressible_by n &
M.3 is_expressible_by n & M.4 is_expressible_by n
proof
let n be non empty Nat,
M be FinSequence of NAT,m,k;
assume that A1: M = IDEA_P(k,n).m and
A2: len m >= 4;
A3: M = IDEAoperationA(IDEAoperationC(IDEAoperationB(m,k,n)),k,n)
by A1,Def15;
len m = len IDEAoperationB(m,k,n) by Def12
.= len IDEAoperationC(IDEAoperationB(m,k,n)) by Def13;
hence thesis by A2,A3,Def11,Th27;
end;
theorem Th44:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
r being Nat holds rng compose(IDEA_P_F(Key,n,r),MESSAGES) c=MESSAGES &
dom compose(IDEA_P_F(Key,n,r),MESSAGES) =MESSAGES
proof
let n be non empty Nat,
lk be Nat,
Key be Matrix of lk,6,NAT, r be Nat;
A1: IDEA_P_F(Key,n,r) is FuncSequence by Th39;
A2: rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= MESSAGES
proof
per cases;
suppose A3: r<>0;
then 0 < r by NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A4:1 <= r & r <= r by NAT_1:38;
r = len IDEA_P_F(Key,n,r) by Def17;
then r in Seg len IDEA_P_F(Key,n,r) by A4,FINSEQ_1:3;
then A5:r in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,r)) <> 0 by A3,Def17;
then A6: not(IDEA_P_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
then lastrng IDEA_P_F(Key,n,r)
= proj2 (IDEA_P_F(Key,n,r).
len (IDEA_P_F(Key,n,r))) by FUNCT_7:def 7
.= proj2 (IDEA_P_F(Key,n,r).r) by Def17
.= proj2 (IDEA_P(Line(Key,r),n)) by A5,Def17
.= rng IDEA_P(Line(Key,r),n) by FUNCT_5:21;
then A7: lastrng IDEA_P_F(Key,n,r) c= MESSAGES
by RELSET_1:12;
rng compose(IDEA_P_F(Key,n,r),MESSAGES)
c= lastrng IDEA_P_F(Key,n,r) by A6,FUNCT_7:61;
hence rng compose(IDEA_P_F(Key,n,r),MESSAGES) c= MESSAGES
by A7,XBOOLE_1:1;
suppose r=0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {} by FINSEQ_1:25;
then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES
by FUNCT_7:41;
hence thesis by FUNCT_2:67;
end;
dom compose(IDEA_P_F(Key,n,r),MESSAGES) = MESSAGES
proof
per cases;
suppose r=0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {} by FINSEQ_1:25;
then compose(IDEA_P_F(Key,n,r),MESSAGES) = id MESSAGES
by FUNCT_7:41;
hence thesis by FUNCT_2:67;
suppose A8: r<>0;
firstdom IDEA_P_F(Key,n,r) = MESSAGES
proof
0 < r by A8,NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A9:1 <= 1 & 1 <= r by NAT_1:38;
r = len IDEA_P_F(Key,n,r) by Def17;
then 1 in Seg len IDEA_P_F(Key,n,r) by A9,FINSEQ_1:3;
then A10:1 in dom IDEA_P_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_P_F(Key,n,r)) <> 0 by A8,Def17;
then not(IDEA_P_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
hence firstdom IDEA_P_F(Key,n,r)
= proj1 (IDEA_P_F(Key,n,r).1) by FUNCT_7:def 6
.= proj1 (IDEA_P(Line(Key,1),n)) by A10,Def17
.= dom IDEA_P(Line(Key,1),n) by FUNCT_5:21
.= MESSAGES by FUNCT_2:def 1;
end;
hence thesis by A1,FUNCT_7:64;
end;
hence thesis by A2;
end;
theorem
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
r being Nat holds rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c=MESSAGES &
dom compose(IDEA_Q_F(Key,n,r),MESSAGES) =MESSAGES
proof
let n be non empty Nat,
lk be Nat,
Key be Matrix of lk,6,NAT, r be Nat;
A1: IDEA_Q_F(Key,n,r) is FuncSequence by Th40;
A2: rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= MESSAGES
proof
per cases;
suppose A3: r<>0;
then 0 < r by NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A4:1 <= r & r <= r by NAT_1:38;
r = len IDEA_Q_F(Key,n,r) by Def18;
then r in Seg len IDEA_Q_F(Key,n,r) by A4,FINSEQ_1:3;
then A5:r in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A3,Def18;
then A6: not(IDEA_Q_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
then lastrng IDEA_Q_F(Key,n,r)
= proj2 (IDEA_Q_F(Key,n,r).
len (IDEA_Q_F(Key,n,r))) by FUNCT_7:def 7
.= proj2 (IDEA_Q_F(Key,n,r).r) by Def18
.= proj2 (IDEA_Q(Line(Key,r-'r+1),n)) by A5,Def18
.= rng IDEA_Q(Line(Key,r-'r+1),n) by FUNCT_5:21;
then A7: lastrng IDEA_Q_F(Key,n,r) c= MESSAGES
by RELSET_1:12;
rng compose(IDEA_Q_F(Key,n,r),MESSAGES)
c= lastrng IDEA_Q_F(Key,n,r) by A6,FUNCT_7:61;
hence rng compose(IDEA_Q_F(Key,n,r),MESSAGES) c= MESSAGES
by A7,XBOOLE_1:1;
suppose r=0;
then len IDEA_Q_F(Key,n,r) = 0 by Def18;
then IDEA_Q_F(Key,n,r) = {} by FINSEQ_1:25;
then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES
by FUNCT_7:41;
hence thesis by FUNCT_2:67;
end;
dom compose(IDEA_Q_F(Key,n,r),MESSAGES) = MESSAGES
proof
per cases;
suppose r=0;
then len IDEA_Q_F(Key,n,r) = 0 by Def18;
then IDEA_Q_F(Key,n,r) = {} by FINSEQ_1:25;
then compose(IDEA_Q_F(Key,n,r),MESSAGES) = id MESSAGES
by FUNCT_7:41;
hence thesis by FUNCT_2:67;
suppose A8: r<>0;
firstdom IDEA_Q_F(Key,n,r) = MESSAGES
proof
0 < r by A8,NAT_1:19;
then 0+1 < r+1 by REAL_1:53;
then A9:1 <= 1 & 1 <= r by NAT_1:38;
r = len IDEA_Q_F(Key,n,r) by Def18;
then 1 in Seg len IDEA_Q_F(Key,n,r) by A9,FINSEQ_1:3;
then A10:1 in dom IDEA_Q_F(Key,n,r) by FINSEQ_1:def 3;
len (IDEA_Q_F(Key,n,r)) <> 0 by A8,Def18;
then not(IDEA_Q_F(Key,n,r)=<*>MESSAGES) by FINSEQ_1:32;
hence firstdom IDEA_Q_F(Key,n,r)
= proj1 (IDEA_Q_F(Key,n,r).1) by FUNCT_7:def 6
.= proj1 (IDEA_Q(Line(Key,r-'1+1),n)) by A10,Def18
.= dom IDEA_Q(Line(Key,r-'1+1),n) by FUNCT_5:21
.= MESSAGES by FUNCT_2:def 1;
end;
hence thesis by A1,FUNCT_7:64;
end;
hence thesis by A2;
end;
theorem Th46:
for n being non empty Nat,m being FinSequence of NAT, lk being Nat,
Key being Matrix of lk,6,NAT, r being Nat,
M being FinSequence of NAT st
M = compose(IDEA_P_F(Key,n,r),MESSAGES).m & len m >= 4
holds len M >= 4
proof
let n be non empty Nat,
m be FinSequence of NAT, lk be Nat,
Key be Matrix of lk,6,NAT;
A1: m in MESSAGES by Def14,FINSEQ_1:def 11;
for r being Nat,M being FinSequence of NAT st
M = compose(IDEA_P_F(Key,n,r),MESSAGES).m & len m >= 4 holds
len M >= 4
proof
defpred P[Nat] means
for M being FinSequence of NAT st
M = compose(IDEA_P_F(Key,n,$1),MESSAGES).m & len m >= 4 holds
len M >= 4;
A2: P[0]
proof
let M be FinSequence of NAT;
assume that A3: M = compose(IDEA_P_F(Key,n,0),MESSAGES).m and
A4: len m >= 4;
len IDEA_P_F(Key,n,0) = 0 by Def17;
then IDEA_P_F(Key,n,0) = {} by FINSEQ_1:25;
then M = (id MESSAGES).m by A3,FUNCT_7:41
.= m by A1,FUNCT_1:35;
hence thesis by A4;
end;
A5: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A6: P[k];
let M be FinSequence of NAT;
assume that A7: M = compose(IDEA_P_F(Key,n,k+1),MESSAGES).m and
A8: len m >= 4;
M = compose(IDEA_P_F(Key,n,k)^<* IDEA_P(Line(Key,(k+1)),n) *>,
MESSAGES).m by A7,Th37;
then A9: M = (IDEA_P(Line(Key,(k+1)),n)*
compose(IDEA_P_F(Key,n,k),MESSAGES)).m by FUNCT_7:43;
A10: dom compose(IDEA_P_F(Key,n,k),MESSAGES) = MESSAGES &
rng compose(IDEA_P_F(Key,n,k),MESSAGES) c= MESSAGES by Th44;
then compose(IDEA_P_F(Key,n,k),MESSAGES).m
in rng(compose(IDEA_P_F(Key,n,k),MESSAGES)) by A1,FUNCT_1:def 5
;
then reconsider M1 = compose(IDEA_P_F(Key,n,k),MESSAGES).m
as FinSequence of NAT by A10,Def14,FINSEQ_1:def 11;
A11:len M1 >= 4 by A6,A8;
dom (IDEA_P(Line(Key,(k+1)),n)*
compose(IDEA_P_F(Key,n,k),MESSAGES))=MESSAGES
proof
rng compose(IDEA_P_F(Key,n,k),MESSAGES)
c= dom IDEA_P(Line(Key,(k+1)),n) by A10,FUNCT_2:def 1;
hence thesis by A10,RELAT_1:46;
end;
then M = IDEA_P(Line(Key,(k+1)),n).
(compose(IDEA_P_F(Key,n,k),MESSAGES).m) by A1,A9,FUNCT_1:22;
hence thesis by A11,Th43;
end;
thus for k being Nat holds P[k] from Ind(A2,A5);
end;
hence thesis;
end;
theorem Th47:
for n being non empty Nat,lk being Nat,Key being Matrix of lk,6,NAT,
r being Nat,M being FinSequence of NAT,m st
M = compose(IDEA_P_F(Key,n,r),MESSAGES).m & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n
holds
len M >= 4 &
M.1 is_expressible_by n &
M.2 is_expressible_by n &
M.3 is_expressible_by n &
M.4 is_expressible_by n
proof
let n be non empty Nat,
lk be Nat,
Key be Matrix of lk,6,NAT, r be Nat,
M be FinSequence of NAT,m;
assume that A1: M = compose(IDEA_P_F(Key,n,r),MESSAGES).m and
A2: len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n;
A3: m in MESSAGES by Def14,FINSEQ_1:def 11;
per cases;
suppose r = 0;
then len IDEA_P_F(Key,n,r) = 0 by Def17;
then IDEA_P_F(Key,n,r) = {} by FINSEQ_1:25;
then M = (id MESSAGES).m by A1,FUNCT_7:41
.= m by A3,FUNCT_1:35;
hence thesis by A2;
suppose A4: r <> 0;
consider r1 being Integer such that A5:r1=r-1;
A6: r1 + 1 = r -(1 - 1) by A5,XCMPLX_1:37
.= r;
1 <= r by A4,RLVECT_1:99;
then 1 - 1 <= r - 1 by REAL_1:49;
then reconsider r1 as Nat by A5,INT_1:16;
IDEA_P_F(Key,n,(r1+1)) =
IDEA_P_F(Key,n,r1)^<* IDEA_P(Line(Key,(r1+1)),n) *> by Th37;
then A7:compose(IDEA_P_F(Key,n,r),MESSAGES) =
IDEA_P(Line(Key,r),n)*compose(IDEA_P_F(Key,n,r1),MESSAGES)
by A6,FUNCT_7:43;
then m in dom(IDEA_P(Line(Key,r),n)*
compose(IDEA_P_F(Key,n,r1),MESSAGES)) by A3,Th44;
then A8: M =
IDEA_P(Line(Key,r),n).(compose(IDEA_P_F(Key,n,r1),MESSAGES).m)
by A1,A7,FUNCT_1:22;
A9: dom compose(IDEA_P_F(Key,n,r1),MESSAGES) = MESSAGES &
rng compose(IDEA_P_F(Key,n,r1),MESSAGES) c= MESSAGES by Th44;
then compose(IDEA_P_F(Key,n,r1),MESSAGES).m
in rng(compose(IDEA_P_F(Key,n,r1),MESSAGES)) by A3,FUNCT_1:def 5;
then reconsider M1 = compose(IDEA_P_F(Key,n,r1),MESSAGES).m
as FinSequence of NAT by A9,Def14,FINSEQ_1:def 11;
len M1 >= 4 by A2,Th46;
hence thesis by A8,Th43;
end;
begin :: Modeling of IDEA Cryptogram
:: IDEA encryption algorithm is as follows:
:: IDEA_PS -> IDEA_P -> IDEA_P -> ... -> IDEA_P -> IDEA_PE
:: IDEA decryption algorithm is as follows:
:: IDEA_QE -> IDEA_Q -> IDEA_Q -> ... -> IDEA_Q -> IDEA_QS
:: Theorem 49 ensures that the ciphertext that is encrypted by IDEA
:: encryption algorithm can be decrypted by IDEA decryption algorithm.
theorem Th48:
for n being non empty Nat,lk being Nat,Key1,Key2 being Matrix of lk,6,NAT,
r being Nat,m st lk >= r &
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
(for i being Nat holds i <= r implies
Key1*(i,1) is_expressible_by n & Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*(i,6) is_expressible_by n &
Key2*(i,1)=INV_MOD(Key1*(i,1),n) & Key2*(i,2)=NEG_MOD(Key1*
(i,3),n) &
Key2*(i,3)=NEG_MOD(Key1*(i,2),n) & Key2*(i,4)=INV_MOD(Key1*
(i,4),n) &
Key1*(i,5)=Key2*(i,5) & Key1*(i,6)=Key2*(i,6))
holds compose(IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r),MESSAGES).m = m
proof
let n be non empty Nat,
lk be Nat;
let Key1,Key2 be Matrix of lk,6,NAT;
for r being Nat st
lk >= r &
2 to_power(n)+1 is prime &
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
(for i being Nat holds i <= r implies
Key1*(i,1) is_expressible_by n & Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*(i,6) is_expressible_by n &
Key2*(i,1) = INV_MOD(Key1*(i,1),n) &
Key2*(i,2) = NEG_MOD(Key1*(i,3),n) &
Key2*(i,3) = NEG_MOD(Key1*(i,2),n) &
Key2*(i,4) = INV_MOD(Key1*(i,4),n) &
Key1*(i,5) = Key2*(i,5) &
Key1*(i,6) = Key2*(i,6))
holds
compose(IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r), MESSAGES).m = m
proof
defpred P[Nat] means
lk >= $1 &
2 to_power(n)+1 is prime &
len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
(for i being Nat holds i <= $1 implies
Key1*(i,1) is_expressible_by n & Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*(i,6) is_expressible_by n &
Key2*(i,1) = INV_MOD(Key1*(i,1),n) &
Key2*(i,2) = NEG_MOD(Key1*(i,3),n) &
Key2*(i,3) = NEG_MOD(Key1*(i,2),n) &
Key2*(i,4) = INV_MOD(Key1*(i,4),n) &
Key1*(i,5) = Key2*(i,5) &
Key1*(i,6) = Key2*(i,6))
implies
compose(IDEA_P_F(Key1,n,$1)^IDEA_Q_F(Key2,n,$1),MESSAGES).m = m;
A1: P[0]
proof
A2: len IDEA_P_F(Key1,n,0) = 0 by Def17;
A3:m in MESSAGES by Def14,FINSEQ_1:def 11;
len IDEA_Q_F(Key2,n,0) = 0 by Def18;
then IDEA_Q_F(Key2,n,0) = {} by FINSEQ_1:25;
then IDEA_P_F(Key1,n,0)^IDEA_Q_F(Key2,n,0)
= IDEA_P_F(Key1,n,0) by FINSEQ_1:47
.= {} by A2,FINSEQ_1:25;
then compose(IDEA_P_F(Key1,n,0)^IDEA_Q_F(Key2,n,0),MESSAGES)
= id MESSAGES by FUNCT_7:41;
hence thesis by A3,FUNCT_1:35;
end;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A5: P[k];
assume that
A6: lk >= k+1 and
A7: 2 to_power(n)+1 is prime and
A8: len m >= 4 and
A9: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n and
A10:(for i being Nat holds i <= k+1 implies
Key1*(i,1) is_expressible_by n &
Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n &
Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n &
Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n &
Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n &
Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n &
Key2*(i,6) is_expressible_by n &
Key2*(i,1) = INV_MOD(Key1*(i,1),n) &
Key2*(i,2) = NEG_MOD(Key1*(i,3),n) &
Key2*(i,3) = NEG_MOD(Key1*(i,2),n) &
Key2*(i,4) = INV_MOD(Key1*(i,4),n) &
Key1*(i,5) = Key2*(i,5) &
Key1*(i,6) = Key2*(i,6));
A11: k+1 >= k by NAT_1:29;
A12:
(for i being Nat holds i <= k implies
Key1*(i,1) is_expressible_by n & Key1*
(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*
(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*
(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*
(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*
(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*
(i,6) is_expressible_by n &
Key2*(i,1) = INV_MOD(Key1*(i,1),n) &
Key2*(i,2) = NEG_MOD(Key1*(i,3),n) &
Key2*(i,3) = NEG_MOD(Key1*(i,2),n) &
Key2*(i,4) = INV_MOD(Key1*(i,4),n) &
Key1*(i,5) = Key2*(i,5) &
Key1*(i,6) = Key2*(i,6))
proof
let i be Nat;
assume i <= k;
then i <= k+1 by A11,AXIOMS:22;
hence thesis by A10;
end;
A13:rng compose(IDEA_P_F(Key1,n,k),MESSAGES) c= MESSAGES by Th44;
A14: rng compose(IDEA_P_F(Key1,n,k)^
(<*IDEA_P(Line(Key1,(k+1)),n)*>^
<*IDEA_Q(Line(Key2,k+1),n)*>),MESSAGES) c= MESSAGES
proof
A15:rng compose(IDEA_P_F(Key1,n,k)^
(<*IDEA_P(Line(Key1,(k+1)),n)*>^
<*IDEA_Q(Line(Key2,k+1),n)*>),MESSAGES)
= rng compose(IDEA_P_F(Key1,n,k)^
<*IDEA_P(Line(Key1,(k+1)),n)*>^
<*IDEA_Q(Line(Key2,k+1),n)*>,MESSAGES) by FINSEQ_1:45
.= rng (IDEA_Q(Line(Key2,k+1),n)*
compose(IDEA_P_F(Key1,n,k)^
<*IDEA_P(Line(Key1,(k+1)),n)*>,MESSAGES)) by FUNCT_7:43;
A16: rng (IDEA_Q(Line(Key2,k+1),n)*
compose(IDEA_P_F(Key1,n,k)^
<*IDEA_P(Line(Key1,(k+1)),n)*>,MESSAGES))
c= rng IDEA_Q(Line(Key2,k+1),n)
proof
let a be set;
assume a in rng (IDEA_Q(Line(Key2,k+1),n)*
compose(IDEA_P_F(Key1,n,k)^
<*IDEA_P(Line(Key1,(k+1)),n)*>,MESSAGES));
hence a in rng IDEA_Q(Line(Key2,k+1),n) by FUNCT_1:25;
end;
rng IDEA_Q(Line(Key2,k+1),n) c= MESSAGES by RELSET_1:12;
hence thesis by A15,A16,XBOOLE_1:1;
end;
A17: dom compose(IDEA_P_F(Key1,n,k),MESSAGES) = MESSAGES by Th44;
A18: dom ((IDEA_Q(Line(Key2,(k+1)),n) *
IDEA_P(Line(Key1,(k+1)),n))*
compose(IDEA_P_F(Key1,n,k),MESSAGES))=MESSAGES
proof
dom (IDEA_Q(Line(Key2,(k+1)),n) *
IDEA_P(Line(Key1,(k+1)),n)) = MESSAGES
by FUNCT_2:def 1;
hence thesis by A13,A17,RELAT_1:46;
end;
A19: m in MESSAGES by Def14,FINSEQ_1:def 11;
then compose(IDEA_P_F(Key1,n,k),MESSAGES).m
in rng(compose(IDEA_P_F(Key1,n,k),MESSAGES))
by A17,FUNCT_1:def 5;
then reconsider M = compose(IDEA_P_F(Key1,n,k),MESSAGES).m
as FinSequence of NAT by A13,Def14,FINSEQ_1:def 11;
A20: len M >= 4 &
M.1 is_expressible_by n &
M.2 is_expressible_by n &
M.3 is_expressible_by n &
M.4 is_expressible_by n by A8,A9,Th47;
lk > 0 by A6,NAT_1:19;
then width Key1 = 6 & width Key2 = 6 by MATRIX_1:24;
then A21: 1 in Seg(width Key1) & 2 in Seg(width Key1) &
3 in Seg(width Key1) & 4 in Seg(width Key1) &
5 in Seg(width Key1) & 6 in Seg(width Key1) &
1 in Seg(width Key2) & 2 in Seg(width Key2) &
3 in Seg(width Key2) & 4 in Seg(width Key2) &
5 in Seg(width Key2) & 6 in Seg(width Key2)
by FINSEQ_1:3;
consider k1 being Nat such that A22: k1 = k+1;
Line(Key1,(k+1)).1 = Key1*(k1,1) &
Line(Key1,(k+1)).2 = Key1*(k1,2) &
Line(Key1,(k+1)).3 = Key1*(k1,3) &
Line(Key1,(k+1)).4 = Key1*(k1,4) &
Line(Key1,(k+1)).5 = Key1*(k1,5) &
Line(Key1,(k+1)).6 = Key1*(k1,6) &
Line(Key2,(k+1)).1 = Key2*(k1,1) &
Line(Key2,(k+1)).2 = Key2*(k1,2) &
Line(Key2,(k+1)).3 = Key2*(k1,3) &
Line(Key2,(k+1)).4 = Key2*(k1,4) &
Line(Key2,(k+1)).5 = Key2*(k1,5) &
Line(Key2,(k+1)).6 = Key2*(k1,6) by A21,A22,MATRIX_1:def 8;
then A23:
Line(Key1,(k+1)).1 is_expressible_by n &
Line(Key1,(k+1)).2 is_expressible_by n &
Line(Key1,(k+1)).3 is_expressible_by n &
Line(Key1,(k+1)).4 is_expressible_by n &
Line(Key1,(k+1)).5 is_expressible_by n &
Line(Key1,(k+1)).6 is_expressible_by n &
Line(Key2,(k+1)).1 = INV_MOD(Line(Key1,(k+1)).1,n) &
Line(Key2,(k+1)).2 = NEG_MOD(Line(Key1,(k+1)).3,n) &
Line(Key2,(k+1)).3 = NEG_MOD(Line(Key1,(k+1)).2,n) &
Line(Key2,(k+1)).4 = INV_MOD(Line(Key1,(k+1)).4,n) &
Line(Key2,(k+1)).5 = Line(Key1,(k+1)).5 &
Line(Key2,(k+1)).6 = Line(Key1,(k+1)).6 by A10,A22;
compose(IDEA_P_F(Key1,n,(k+1))^IDEA_Q_F(Key2,n,(k+1)),
MESSAGES).m
= compose((IDEA_P_F(Key1,n,k)^<* IDEA_P(Line(Key1,(k+1)),n) *>)
^IDEA_Q_F(Key2,n,(k+1)),MESSAGES).m by Th37
.= compose((IDEA_P_F(Key1,n,k)^<*IDEA_P(Line(Key1,(k+1)),n)*>)^
(<*IDEA_Q(Line(Key2,(k+1)),n)*>^IDEA_Q_F(Key2,n,k)),MESSAGES).m
by Th38
.= compose(IDEA_P_F(Key1,n,k)^<*IDEA_P(Line(Key1,(k+1)),n)*>^
<*IDEA_Q(Line(Key2,(k+1)),n)*>^IDEA_Q_F(Key2,n,k),MESSAGES).m
by FINSEQ_1:45
.= compose(IDEA_P_F(Key1,n,k)^
(<*IDEA_P(Line(Key1,(k+1)),n)*>^<*IDEA_Q(Line(Key2,(k+1)),n)*>)^
IDEA_Q_F(Key2,n,k),MESSAGES).m by FINSEQ_1:45
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
compose(IDEA_P_F(Key1,n,k)^
(<*IDEA_P(Line(Key1,(k+1)),n)*>^<*IDEA_Q(Line(Key2,(k+1)),n)*>)
,MESSAGES)).m by A14,FUNCT_7:50
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
(compose(<*IDEA_P(Line(Key1,(k+1)),n)*>^
<*IDEA_Q(Line(Key2,(k+1)),n)*>,MESSAGES) *
compose(IDEA_P_F(Key1,n,k),MESSAGES))).m by A13,FUNCT_7:50
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
(compose(<*IDEA_P(Line(Key1,(k+1)),n),
IDEA_Q(Line(Key2,(k+1)),n)*>,MESSAGES) *
compose(IDEA_P_F(Key1,n,k),MESSAGES))).m by FINSEQ_1:def 9
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
((IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n)
* id MESSAGES) *
compose(IDEA_P_F(Key1,n,k),MESSAGES))).m by FUNCT_7:53
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
((IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n))*
compose(IDEA_P_F(Key1,n,k),MESSAGES))).m by FUNCT_2:74
.= compose(IDEA_Q_F(Key2,n,k),MESSAGES).
(((IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n))*
compose(IDEA_P_F(Key1,n,k),MESSAGES)).m)
by A18,A19,FUNCT_1:23
.= compose(IDEA_Q_F(Key2,n,k),MESSAGES).
((IDEA_Q(Line(Key2,(k+1)),n) * IDEA_P(Line(Key1,(k+1)),n)).
((compose(IDEA_P_F(Key1,n,k),MESSAGES)).m))
by A17,A19,FUNCT_1:23
.= compose(IDEA_Q_F(Key2,n,k),MESSAGES).
(compose(IDEA_P_F(Key1,n,k),MESSAGES).m)
by A7,A20,A23,Th34
.=(compose(IDEA_Q_F(Key2,n,k),MESSAGES) *
compose(IDEA_P_F(Key1,n,k),MESSAGES)).m
by A17,A19,FUNCT_1:23
.= m by A5,A6,A7,A8,A9,A11,A12,A13,AXIOMS:22,FUNCT_7:50;
hence thesis;
end;
thus for k being Nat holds P[k] from Ind(A1,A4);
end;
hence thesis;
end;
theorem
for n being non empty Nat,lk being Nat,Key1,Key2 being Matrix of lk,6,NAT,
r being Nat,ks1,ks2,ke1,ke2 being FinSequence of NAT,m st lk >= r &
2 to_power(n)+1 is prime & len m >= 4 &
m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n &
(for i being Nat holds i <= r implies
Key1*(i,1) is_expressible_by n & Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*(i,6) is_expressible_by n &
Key2*(i,1)=INV_MOD(Key1*(i,1),n) & Key2*(i,2)=NEG_MOD(Key1*
(i,3),n) &
Key2*(i,3)=NEG_MOD(Key1*(i,2),n) & Key2*(i,4)=INV_MOD(Key1*
(i,4),n) &
Key1*(i,5)=Key2*(i,5) & Key1*(i,6)=Key2*(i,6))&
ks1.1 is_expressible_by n & ks1.2 is_expressible_by n &
ks1.3 is_expressible_by n & ks1.4 is_expressible_by n &
ks2.1 = INV_MOD(ks1.1,n) & ks2.2 = NEG_MOD(ks1.2,n) &
ks2.3 = NEG_MOD(ks1.3,n) & ks2.4 = INV_MOD(ks1.4,n) &
ke1.1 is_expressible_by n & ke1.2 is_expressible_by n &
ke1.3 is_expressible_by n & ke1.4 is_expressible_by n &
ke1.5 is_expressible_by n & ke1.6 is_expressible_by n &
ke2.1 = INV_MOD(ke1.1,n) & ke2.2 = NEG_MOD(ke1.2,n) &
ke2.3 = NEG_MOD(ke1.3,n) & ke2.4 = INV_MOD(ke1.4,n) &
ke2.5 = ke1.5 & ke2.6 = ke1.6
holds (IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,r),MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),MESSAGES)*
IDEA_PS(ks1,n)))))).m = m
proof
let n be non empty Nat,
lk be Nat,
Key1,Key2 be Matrix of lk,6,NAT,
r be Nat,
ks1,ks2,ke1,ke2 be FinSequence of NAT,m;
assume that
A1: lk >= r and
A2: 2 to_power(n)+1 is prime &
len m >= 4 and
A3: m.1 is_expressible_by n & m.2 is_expressible_by n &
m.3 is_expressible_by n & m.4 is_expressible_by n and
A4: (for i being Nat holds i <= r implies
Key1*(i,1) is_expressible_by n & Key1*(i,2) is_expressible_by n &
Key1*(i,3) is_expressible_by n & Key1*(i,4) is_expressible_by n &
Key1*(i,5) is_expressible_by n & Key1*(i,6) is_expressible_by n &
Key2*(i,1) is_expressible_by n & Key2*(i,2) is_expressible_by n &
Key2*(i,3) is_expressible_by n & Key2*(i,4) is_expressible_by n &
Key2*(i,5) is_expressible_by n & Key2*(i,6) is_expressible_by n &
Key2*(i,1) = INV_MOD(Key1*(i,1),n) &
Key2*(i,2) = NEG_MOD(Key1*(i,3),n) &
Key2*(i,3) = NEG_MOD(Key1*(i,2),n) &
Key2*(i,4) = INV_MOD(Key1*(i,4),n) &
Key1*(i,5) = Key2*(i,5) &
Key1*(i,6) = Key2*(i,6)) and
A5: ks1.1 is_expressible_by n & ks1.2 is_expressible_by n &
ks1.3 is_expressible_by n & ks1.4 is_expressible_by n &
ks2.1 = INV_MOD(ks1.1,n) & ks2.2 = NEG_MOD(ks1.2,n) &
ks2.3 = NEG_MOD(ks1.3,n) & ks2.4 = INV_MOD(ks1.4,n) and
A6: ke1.1 is_expressible_by n & ke1.2 is_expressible_by n &
ke1.3 is_expressible_by n & ke1.4 is_expressible_by n &
ke1.5 is_expressible_by n & ke1.6 is_expressible_by n &
ke2.1 = INV_MOD(ke1.1,n) & ke2.2 = NEG_MOD(ke1.2,n) &
ke2.3 = NEG_MOD(ke1.3,n) & ke2.4 = INV_MOD(ke1.4,n) &
ke2.5 = ke1.5 & ke2.6 = ke1.6;
A7: m in MESSAGES by Def14,FINSEQ_1:def 11;
then IDEA_PS(ks1,n).m in MESSAGES by FUNCT_2:7;
then reconsider m1 = IDEA_PS(ks1,n).m as FinSequence of NAT
by Def14,FINSEQ_1:def 11;
A8: len m1 = len IDEAoperationA(m,ks1,n) by Def19
.= len m by Def11;
m1.1 = IDEAoperationA(m,ks1,n).1 & m1.2 = IDEAoperationA(m,ks1,n).2 &
m1.3 = IDEAoperationA(m,ks1,n).3 & m1.4 = IDEAoperationA(m,ks1,n).4
by Def19;
then A9:
m1.1 is_expressible_by n &
m1.2 is_expressible_by n &
m1.3 is_expressible_by n &
m1.4 is_expressible_by n by A2,Th27;
A10: m1 in MESSAGES by Def14,FINSEQ_1:def 11;
per cases;
suppose A11: r = 0;
then len IDEA_P_F(Key1,n,r) = 0 by Def17;
then A12: IDEA_P_F(Key1,n,r) = {} by FINSEQ_1:25;
len IDEA_Q_F(Key2,n,r) = 0 by A11,Def18;
hence
(IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,r),MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),MESSAGES)*
IDEA_PS(ks1,n)))))).m
=(IDEA_QS(ks2,n)*(compose({},MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose({},MESSAGES)*
IDEA_PS(ks1,n)))))).m by A12,FINSEQ_1:25
.=(IDEA_QS(ks2,n)*((id MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose({},MESSAGES)*
IDEA_PS(ks1,n)))))).m by FUNCT_7:41
.=(IDEA_QS(ks2,n)*((id MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*((id MESSAGES)*
IDEA_PS(ks1,n)))))).m by FUNCT_7:41
.=(IDEA_QS(ks2,n)*((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*((id MESSAGES)*
IDEA_PS(ks1,n)))))).m by FUNCT_2:74
.=(IDEA_QS(ks2,n)*(IDEA_QE(ke2,n)*
(IDEA_PE(ke1,n)*IDEA_PS(ks1,n)))).m by FUNCT_2:74
.=IDEA_QS(ks2,n).((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*
IDEA_PS(ks1,n))).m) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(IDEA_QE(ke2,n).((IDEA_PE(ke1,n)*
IDEA_PS(ks1,n)).m)) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).m1)) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).((IDEA_QE(ke2,n)*IDEA_PE(ke1,n)).m1)
by A10,FUNCT_2:70
.=IDEA_QS(ks2,n).(IDEA_PS(ks1,n).m) by A2,A6,A8,A9,Th36
.=(IDEA_QS(ks2,n)*IDEA_PS(ks1,n)).m by A7,FUNCT_2:70
.= m by A2,A3,A5,Th35;
suppose r <> 0;
then A13: IDEA_P_F(Key1,n,r) is FuncSequence of MESSAGES,MESSAGES &
IDEA_Q_F(Key2,n,r) is FuncSequence of MESSAGES,MESSAGES
by Th41,Th42;
compose(IDEA_P_F(Key1,n,r),MESSAGES) is Function of MESSAGES,MESSAGES
proof
A14: firstdom IDEA_P_F(Key1,n,r) = MESSAGES &
lastrng IDEA_P_F(Key1,n,r) c= MESSAGES by A13,FUNCT_7:def 9;
then IDEA_P_F(Key1,n,r) = {} implies
rng compose(IDEA_P_F(Key1,n,r),MESSAGES) = {} by FUNCT_7:def 6;
then rng compose(IDEA_P_F(Key1,n,r),MESSAGES)
c= lastrng IDEA_P_F(Key1,n,r) by FUNCT_7:61,XBOOLE_1:2;
then A15:
rng compose(IDEA_P_F(Key1,n,r),MESSAGES) c= MESSAGES
by A14,XBOOLE_1:1;
dom compose(IDEA_P_F(Key1,n,r),MESSAGES)
= MESSAGES by A13,A14,FUNCT_7:64;
hence thesis by A15,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider PF=compose(IDEA_P_F(Key1,n,r),MESSAGES)
as Function of MESSAGES,MESSAGES;
compose(IDEA_Q_F(Key2,n,r),MESSAGES) is Function of MESSAGES,MESSAGES
proof
A16: firstdom IDEA_Q_F(Key2,n,r) = MESSAGES &
lastrng IDEA_Q_F(Key2,n,r) c= MESSAGES by A13,FUNCT_7:def 9;
then IDEA_Q_F(Key2,n,r) = {} implies
rng compose(IDEA_Q_F(Key2,n,r),MESSAGES) = {} by FUNCT_7:def 6;
then rng compose(IDEA_Q_F(Key2,n,r),MESSAGES)
c= lastrng IDEA_Q_F(Key2,n,r) by FUNCT_7:61,XBOOLE_1:2;
then A17:
rng compose(IDEA_Q_F(Key2,n,r),MESSAGES) c= MESSAGES
by A16,XBOOLE_1:1;
dom compose(IDEA_Q_F(Key2,n,r),MESSAGES)
= MESSAGES by A13,A16,FUNCT_7:64;
hence thesis by A17,FUNCT_2:def 1,RELSET_1:11;
end;
then reconsider QF=compose(IDEA_Q_F(Key2,n,r),MESSAGES)
as Function of MESSAGES,MESSAGES;
A18: rng PF c= MESSAGES & rng QF c= MESSAGES by RELSET_1:12;
PF.m1 in MESSAGES by A10,FUNCT_2:7;
then reconsider m2 = PF.m1 as FinSequence of NAT
by Def14,FINSEQ_1:def 11;
A19: len m2 >= 4 &
m2.1 is_expressible_by n &
m2.2 is_expressible_by n &
m2.3 is_expressible_by n &
m2.4 is_expressible_by n by A2,A8,A9,Th47;
A20: m2 in MESSAGES by Def14,FINSEQ_1:def 11;
A21:QF.(PF.m1) = m1
proof
thus
QF.(PF.m1)
= (QF*PF).m1 by A10,FUNCT_2:70
.= compose(IDEA_P_F(Key1,n,r)^IDEA_Q_F(Key2,n,r),MESSAGES).m1
by A18,FUNCT_7:50
.= m1 by A1,A2,A4,A8,A9,Th48;
end;
thus
(IDEA_QS(ks2,n)*(compose(IDEA_Q_F(Key2,n,r),MESSAGES)*
(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(compose(IDEA_P_F(Key1,n,r),MESSAGES)*
IDEA_PS(ks1,n)))))).m
=IDEA_QS(ks2,n).((QF*(IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(PF*
(IDEA_PS(ks1,n)))))).m) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(QF.((IDEA_QE(ke2,n)*(IDEA_PE(ke1,n)*(PF*
(IDEA_PS(ks1,n))))).m)) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).((IDEA_PE(ke1,n)*(PF*
(IDEA_PS(ks1,n)))).m))) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).((PF*
(IDEA_PS(ks1,n))).m)))) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(QF.(IDEA_QE(ke2,n).(IDEA_PE(ke1,n).(PF.
(IDEA_PS(ks1,n).m))))) by A7,FUNCT_2:70
.=IDEA_QS(ks2,n).(QF.((IDEA_QE(ke2,n)*IDEA_PE(ke1,n)).m2))
by A20,FUNCT_2:70
.=IDEA_QS(ks2,n).(m1) by A2,A6,A19,A21,Th36
.=(IDEA_QS(ks2,n)*IDEA_PS(ks1,n)).m by A7,FUNCT_2:70
.= m by A2,A3,A5,Th35;
end;