let n be non zero Nat; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 :: thesis: for j being Nat st j in Seg (len m) holds
I2 . j = m . j

let j be Nat; :: thesis: ( j in Seg (len m) implies I2 . j = m . j )
assume A22: j in Seg (len m) ; :: thesis: I2 . j = m . j
then 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 :: thesis: I2 . j = m . j

per cases ( j = 1 or j = 2 or j = 3 or j = 4 or ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ) ;

suppose A25: j = 1 ; :: thesis: I2 . j = m . j

A26: m . 1 < 2 to_power n by A2;
thus I2 . j = Absval ((n -BinarySequence (I1 . 1)) 'xor' (n -BinarySequence t11)) by A12, A15, A18, A20, A23, A25, Def12
.= Absval (((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence t11)) 'xor' (n -BinarySequence t11)) by A11, BINARI_3:36
.= Absval ((n -BinarySequence (m . 1)) 'xor' ((n -BinarySequence t11) 'xor' (n -BinarySequence t11))) by Th9
.= Absval ((ZERO n) 'xor' (n -BinarySequence (m . 1))) by Th6
.= Absval (n -BinarySequence (m . 1)) by Th8
.= m . j by A25, A26, BINARI_3:35 ; :: thesis: verum

end;

suppose A27: j = 2 ; :: thesis: I2 . j = m . j

A28: 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 ; :: thesis: verum

end;

suppose A29: j = 3 ; :: thesis: I2 . j = m . j

A30: m . 3 < 2 to_power n by A4;
thus I2 . j = Absval ((n -BinarySequence (I1 . 3)) 'xor' (n -BinarySequence t11)) by A12, A15, A18, A20, A23, A29, Def12
.= Absval (((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence t11)) 'xor' (n -BinarySequence t11)) by A13, BINARI_3:36
.= Absval ((n -BinarySequence (m . 3)) 'xor' ((n -BinarySequence t11) 'xor' (n -BinarySequence t11))) by Th9
.= Absval ((ZERO n) 'xor' (n -BinarySequence (m . 3))) by Th6
.= Absval (n -BinarySequence (m . 3)) by Th8
.= m . j by A29, A30, BINARI_3:35 ; :: thesis: verum

end;

suppose A31: j = 4 ; :: thesis: I2 . j = m . j

A32: 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 ; :: thesis: verum

end;

suppose A33: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis: I2 . j = m . j

hence I2 . j = I1 . j by A18, A23, Def12
.= m . j by A10, A24, A33, Def12 ;
:: thesis: verum

end;

end;

end;

hence I2 . j = m . j ; :: thesis: 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; :: thesis: verum