let n be non zero Nat; for m, k1, k2 being FinSequence of NAT st (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) holds
IDEAoperationA ((IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),k2,n) = m
let m, k1, k2 be FinSequence of NAT ; ( (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 )
assume that
A1:
(2 to_power n) + 1 is prime
and
A2:
len m >= 4
and
A3:
m . 1 is_expressible_by n
and
A4:
m . 2 is_expressible_by n
and
A5:
m . 3 is_expressible_by n
and
A6:
m . 4 is_expressible_by n
and
A7:
k1 . 1 is_expressible_by n
and
A8:
k1 . 2 is_expressible_by n
and
A9:
k1 . 3 is_expressible_by n
and
A10:
k1 . 4 is_expressible_by n
and
A11:
k2 . 1 = INV_MOD ((k1 . 1),n)
and
A12:
k2 . 2 = NEG_MOD ((k1 . 3),n)
and
A13:
k2 . 3 = NEG_MOD ((k1 . 2),n)
and
A14:
k2 . 4 = INV_MOD ((k1 . 4),n)
; IDEAoperationA ((IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),k2,n) = m
A15:
k2 . 1 is_expressible_by n
by A1, A7, A11, Def10;
1 <= len m
by A2, XXREAL_0:2;
then A16:
1 in Seg (len m)
by FINSEQ_1:1;
then A17:
1 in dom m
by FINSEQ_1:def 3;
A18:
4 in Seg (len m)
by A2, FINSEQ_1:1;
then A19:
4 in dom m
by FINSEQ_1:def 3;
3 <= len m
by A2, XXREAL_0:2;
then A20:
3 in Seg (len m)
by FINSEQ_1:1;
then A21:
3 in dom m
by FINSEQ_1:def 3;
A22:
k2 . 4 is_expressible_by n
by A1, A10, A14, Def10;
consider I1 being FinSequence of NAT such that
A23:
I1 = IDEAoperationC m
;
4 in Seg (len I1)
by A23, A18, Def13;
then A24:
4 in dom I1
by FINSEQ_1:def 3;
1 in Seg (len I1)
by A23, A16, Def13;
then A25:
1 in dom I1
by FINSEQ_1:def 3;
2 <= len m
by A2, XXREAL_0:2;
then A26:
2 in Seg (len m)
by FINSEQ_1:1;
then A27:
2 in dom m
by FINSEQ_1:def 3;
3 in Seg (len I1)
by A23, A20, Def13;
then A28:
3 in dom I1
by FINSEQ_1:def 3;
2 in Seg (len I1)
by A23, A26, Def13;
then A29:
2 in dom I1
by FINSEQ_1:def 3;
consider I2 being FinSequence of NAT such that
A30:
I2 = IDEAoperationA (I1,k1,n)
;
A31:
len I2 = len I1
by A30, Def11;
then
2 in Seg (len I2)
by A23, A26, Def13;
then A32:
2 in dom I2
by FINSEQ_1:def 3;
4 in Seg (len I2)
by A23, A31, A18, Def13;
then A33:
4 in dom I2
by FINSEQ_1:def 3;
1 in Seg (len I2)
by A23, A31, A16, Def13;
then A34:
1 in dom I2
by FINSEQ_1:def 3;
3 in Seg (len I2)
by A23, A31, A20, Def13;
then A35:
3 in dom I2
by FINSEQ_1:def 3;
consider I3 being FinSequence of NAT such that
A36:
I3 = IDEAoperationC I2
;
A37:
len I3 = len I2
by A36, Def13;
then
2 in Seg (len I3)
by A23, A31, A26, Def13;
then A38:
2 in dom I3
by FINSEQ_1:def 3;
4 in Seg (len I3)
by A23, A31, A37, A18, Def13;
then A39:
4 in dom I3
by FINSEQ_1:def 3;
3 in Seg (len I3)
by A23, A31, A37, A20, Def13;
then A40:
3 in dom I3
by FINSEQ_1:def 3;
consider I4 being FinSequence of NAT such that
A41:
I4 = IDEAoperationA (I3,k2,n)
;
1 in Seg (len I3)
by A23, A31, A37, A16, Def13;
then A42:
1 in dom I3
by FINSEQ_1:def 3;
A43:
now for j being Nat st j in Seg (len m) holds
I4 . j = m . jlet j be
Nat;
( j in Seg (len m) implies I4 . j = m . j )assume A44:
j in Seg (len m)
;
I4 . j = m . jthen A45:
j in dom m
by FINSEQ_1:def 3;
A46:
j in Seg (len I1)
by A23, A44, Def13;
then A47:
j in Seg (len I2)
by A30, Def11;
then A48:
j in dom I2
by FINSEQ_1:def 3;
j in Seg (len I3)
by A36, A47, Def13;
then A49:
j in dom I3
by FINSEQ_1:def 3;
A50:
j in dom I1
by A46, FINSEQ_1:def 3;
now I4 . j = m . jper cases
( j = 1 or j = 2 or j = 3 or j = 4 or ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) )
;
suppose A51:
j = 1
;
I4 . j = m . jhence I4 . j =
MUL_MOD (
(I3 . 1),
(k2 . 1),
n)
by A41, A42, Def11
.=
MUL_MOD (
(I2 . 1),
(k2 . 1),
n)
by A36, A34, Lm5
.=
MUL_MOD (
(MUL_MOD ((I1 . 1),(k1 . 1),n)),
(k2 . 1),
n)
by A30, A25, Def11
.=
MUL_MOD (
(MUL_MOD ((m . 1),(k1 . 1),n)),
(k2 . 1),
n)
by A23, A17, Lm5
.=
MUL_MOD (
(m . 1),
(MUL_MOD ((k1 . 1),(k2 . 1),n)),
n)
by A1, A3, A7, A15, Th23
.=
MUL_MOD (1,
(m . 1),
n)
by A1, A7, A11, Def10
.=
m . j
by A3, A51, Th22
;
verum end; suppose A52:
j = 2
;
I4 . j = m . jhence I4 . j =
ADD_MOD (
(I3 . 2),
(k2 . 2),
n)
by A41, A38, Def11
.=
ADD_MOD (
(I2 . 3),
(k2 . 2),
n)
by A36, A32, Lm3
.=
ADD_MOD (
(ADD_MOD ((I1 . 3),(k1 . 3),n)),
(k2 . 2),
n)
by A30, A28, Def11
.=
ADD_MOD (
(ADD_MOD ((m . 2),(k1 . 3),n)),
(k2 . 2),
n)
by A23, A21, Lm4
.=
ADD_MOD (
(m . 2),
(ADD_MOD ((k1 . 3),(k2 . 2),n)),
n)
by Th14
.=
ADD_MOD (
0,
(m . 2),
n)
by A9, A12, Th11
.=
m . j
by A4, A52, Th13
;
verum end; suppose A53:
j = 3
;
I4 . j = m . jhence I4 . j =
ADD_MOD (
(I3 . 3),
(k2 . 3),
n)
by A41, A40, Def11
.=
ADD_MOD (
(I2 . 2),
(k2 . 3),
n)
by A36, A35, Lm4
.=
ADD_MOD (
(ADD_MOD ((I1 . 2),(k1 . 2),n)),
(k2 . 3),
n)
by A30, A29, Def11
.=
ADD_MOD (
(ADD_MOD ((m . 3),(k1 . 2),n)),
(k2 . 3),
n)
by A23, A27, Lm3
.=
ADD_MOD (
(m . 3),
(ADD_MOD ((k1 . 2),(k2 . 3),n)),
n)
by Th14
.=
ADD_MOD (
0,
(m . 3),
n)
by A8, A13, Th11
.=
m . j
by A5, A53, Th13
;
verum end; suppose A54:
j = 4
;
I4 . j = m . jhence I4 . j =
MUL_MOD (
(I3 . 4),
(k2 . 4),
n)
by A41, A39, Def11
.=
MUL_MOD (
(I2 . 4),
(k2 . 4),
n)
by A36, A33, Lm5
.=
MUL_MOD (
(MUL_MOD ((I1 . 4),(k1 . 4),n)),
(k2 . 4),
n)
by A30, A24, Def11
.=
MUL_MOD (
(MUL_MOD ((m . 4),(k1 . 4),n)),
(k2 . 4),
n)
by A23, A19, Lm5
.=
MUL_MOD (
(m . 4),
(MUL_MOD ((k1 . 4),(k2 . 4),n)),
n)
by A1, A6, A10, A22, Th23
.=
MUL_MOD (1,
(m . 4),
n)
by A1, A10, A14, Def10
.=
m . j
by A6, A54, Th22
;
verum end; suppose A55:
(
j <> 1 &
j <> 2 &
j <> 3 &
j <> 4 )
;
I4 . j = m . jhence I4 . j =
I3 . j
by A41, A49, Def11
.=
I2 . j
by A36, A48, A55, Lm5
.=
I1 . j
by A30, A50, A55, Def11
.=
m . j
by A23, A45, A55, Lm5
;
verum end; hence
I4 . j = m . j
;
verum end;
A56:
Seg (len m) = dom m
by FINSEQ_1:def 3;
Seg (len m) =
Seg (len I1)
by A23, Def13
.=
Seg (len I2)
by A30, Def11
.=
Seg (len I3)
by A36, Def13
.=
Seg (len I4)
by A41, Def11
.=
dom I4
by FINSEQ_1:def 3
;
hence
IDEAoperationA ((IDEAoperationC (IDEAoperationA ((IDEAoperationC m),k1,n))),k2,n) = m
by A23, A30, A36, A41, A56, A43, FINSEQ_1:13; verum