let n be non zero Nat; for m, k1, k2 being FinSequence of NAT st 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 & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 holds
IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m
let m, k1, k2 be FinSequence of NAT ; ( 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 & k2 . 5 = k1 . 5 & k2 . 6 = k1 . 6 implies IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m )
assume that
A1:
len m >= 4
and
A2:
m . 1 is_expressible_by n
and
A3:
m . 2 is_expressible_by n
and
A4:
m . 3 is_expressible_by n
and
A5:
m . 4 is_expressible_by n
and
A6:
k2 . 5 = k1 . 5
and
A7:
k2 . 6 = k1 . 6
; IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m
consider t10 being Nat such that
A8:
t10 = MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k1 . 5),n)
;
consider t11 being Nat such that
A9:
t11 = MUL_MOD ((ADD_MOD (t10,(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k1 . 6),n)
;
consider I1 being FinSequence of NAT such that
A10:
I1 = IDEAoperationB (m,k1,n)
;
1 <= len m
by A1, XXREAL_0:2;
then
1 in Seg (len m)
by FINSEQ_1:1;
then
1 in dom m
by FINSEQ_1:def 3;
then A11:
I1 . 1 = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence t11))
by A8, A9, A10, Def12;
consider t20 being Nat such that
A12:
t20 = MUL_MOD ((Absval ((n -BinarySequence (I1 . 1)) 'xor' (n -BinarySequence (I1 . 3)))),(k2 . 5),n)
;
3 <= len m
by A1, XXREAL_0:2;
then
3 in Seg (len m)
by FINSEQ_1:1;
then
3 in dom m
by FINSEQ_1:def 3;
then A13:
I1 . 3 = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence t11))
by A8, A9, A10, Def12;
then A14: 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 A12, A11, BINARI_3:36
.=
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:36
.=
MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' ((n -BinarySequence t11) 'xor' ((n -BinarySequence t11) 'xor' (n -BinarySequence (m . 3)))))),(k2 . 5),n)
by Th9
.=
MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (((n -BinarySequence t11) 'xor' (n -BinarySequence t11)) 'xor' (n -BinarySequence (m . 3))))),(k2 . 5),n)
by Th9
.=
MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' ((ZERO n) 'xor' (n -BinarySequence (m . 3))))),(k2 . 5),n)
by Th6
.=
t10
by A6, A8, Th8
;
consider t21 being Nat such that
A15:
t21 = MUL_MOD ((ADD_MOD (t20,(Absval ((n -BinarySequence (I1 . 2)) 'xor' (n -BinarySequence (I1 . 4)))),n)),(k2 . 6),n)
;
consider t12 being Nat such that
A16:
t12 = ADD_MOD (t10,t11,n)
;
2 <= len m
by A1, XXREAL_0:2;
then
2 in Seg (len m)
by FINSEQ_1:1;
then
2 in dom m
by FINSEQ_1:def 3;
then A17:
I1 . 2 = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence t12))
by A8, A9, A16, A10, Def12;
consider I2 being FinSequence of NAT such that
A18:
I2 = IDEAoperationB (I1,k2,n)
;
4 in Seg (len m)
by A1, FINSEQ_1:1;
then
4 in dom m
by FINSEQ_1:def 3;
then A19:
I1 . 4 = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence t12))
by A8, A9, A16, A10, Def12;
then A20: 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 A15, A17, A14, BINARI_3:36
.=
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:36
.=
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 Th9
.=
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 Th9
.=
MUL_MOD ((ADD_MOD (t10,(Absval ((n -BinarySequence (m . 2)) 'xor' ((ZERO n) 'xor' (n -BinarySequence (m . 4))))),n)),(k2 . 6),n)
by Th6
.=
t11
by A7, A9, Th8
;
A21:
now for j being Nat st j in Seg (len m) holds
I2 . j = m . jlet j be
Nat;
( j in Seg (len m) implies I2 . j = m . j )assume A22:
j in Seg (len m)
;
I2 . j = m . jthen
j in Seg (len I1)
by A10, Def12;
then A23:
j in dom I1
by FINSEQ_1:def 3;
A24:
j in dom m
by A22, FINSEQ_1:def 3;
now I2 . 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 A27:
j = 2
;
I2 . j = m . jA28:
m . 2
< 2
to_power n
by A3;
thus I2 . j =
Absval ((n -BinarySequence (I1 . 2)) 'xor' (n -BinarySequence t12))
by A16, A12, A15, A18, A14, A20, A23, A27, Def12
.=
Absval (((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence t12)) 'xor' (n -BinarySequence t12))
by A17, BINARI_3:36
.=
Absval ((n -BinarySequence (m . 2)) 'xor' ((n -BinarySequence t12) 'xor' (n -BinarySequence t12)))
by Th9
.=
Absval ((ZERO n) 'xor' (n -BinarySequence (m . 2)))
by Th6
.=
Absval (n -BinarySequence (m . 2))
by Th8
.=
m . j
by A27, A28, BINARI_3:35
;
verum end; suppose A31:
j = 4
;
I2 . j = m . jA32:
m . 4
< 2
to_power n
by A5;
thus I2 . j =
Absval ((n -BinarySequence (I1 . 4)) 'xor' (n -BinarySequence t12))
by A16, A12, A15, A18, A14, A20, A23, A31, Def12
.=
Absval (((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence t12)) 'xor' (n -BinarySequence t12))
by A19, BINARI_3:36
.=
Absval ((n -BinarySequence (m . 4)) 'xor' ((n -BinarySequence t12) 'xor' (n -BinarySequence t12)))
by Th9
.=
Absval ((ZERO n) 'xor' (n -BinarySequence (m . 4)))
by Th6
.=
Absval (n -BinarySequence (m . 4))
by Th8
.=
m . j
by A31, A32, BINARI_3:35
;
verum end; end; end; hence
I2 . j = m . j
;
verum end;
A34:
Seg (len m) = dom m
by FINSEQ_1:def 3;
Seg (len m) =
Seg (len I1)
by A10, Def12
.=
Seg (len I2)
by A18, Def12
.=
dom I2
by FINSEQ_1:def 3
;
hence
IDEAoperationB ((IDEAoperationB (m,k1,n)),k2,n) = m
by A10, A18, A34, A21, FINSEQ_1:13; verum