let n be non empty Element of NAT ; :: thesis: 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 . 5 is_expressible_by n & k1 . 6 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: ( (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 )
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 ; :: thesis: IDEAoperationB (IDEAoperationB m,k1,n),k2,n = m
consider t10 being Element of NAT such that
A4: t10 = MUL_MOD (Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k1 . 5),n ;
consider t11 being Element of 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 Element of 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 Element of NAT such that
A8: t20 = MUL_MOD (Absval ((n -BinarySequence (I1 . 1)) 'xor' (n -BinarySequence (I1 . 3)))),(k2 . 5),n ;
consider t21 being Element of 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, XXREAL_0:2;
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, XXREAL_0:2;
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, XXREAL_0:2;
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; :: thesis: ( j in Seg (len m) implies I2 . j = m . j )
assume A19: j in Seg (len m) ; :: thesis: I2 . j = m . j
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 ( j = 1 or j = 2 or j = 3 or j = 4 or ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ) ;
suppose A22: j = 1 ; :: thesis: I2 . j = m . j
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 ; :: thesis: verum
end;
suppose A24: j = 2 ; :: thesis: I2 . j = m . j
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 ; :: thesis: verum
end;
suppose A26: j = 3 ; :: thesis: I2 . j = m . j
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 ; :: thesis: verum
end;
suppose A28: j = 4 ; :: thesis: I2 . j = m . j
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 ; :: thesis: verum
end;
suppose A30: ( j <> 1 & j <> 2 & j <> 3 & j <> 4 ) ; :: thesis: I2 . j = m . j
hence I2 . j = I1 . j by A10, A20, Def12
.= m . j by A7, A21, A30, Def12 ;
:: thesis: verum
end;
end;
end;
hence I2 . j = m . j ; :: thesis: verum
end;
hence IDEAoperationB (IDEAoperationB m,k1,n),k2,n = m by A7, A10, A11, A12, FINSEQ_1:17; :: thesis: verum