let n be non zero Nat; for lk being Nat
for Key being Matrix of lk,6,NAT
for r being Nat
for M, m being FinSequence of NAT 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 )
let lk be Nat; for Key being Matrix of lk,6,NAT
for r being Nat
for M, m being FinSequence of NAT 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 )
let Key be Matrix of lk,6,NAT; for r being Nat
for M, m being FinSequence of NAT 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 )
let r be Nat; for M, m being FinSequence of NAT 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 )
let M, m be FinSequence of NAT ; ( 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 implies ( 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 ) )
assume that
A1:
M = (compose ((IDEA_P_F (Key,n,r)),MESSAGES)) . m
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 )
; ( 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 )
A4:
m in MESSAGES
by FINSEQ_1:def 11;
per cases
( r = 0 or r <> 0 )
;
suppose A5:
r <> 0
;
( 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 )consider r1 being
Integer such that A6:
r1 = r - 1
;
defpred S1[
Nat]
means for
M being
FinSequence of
NAT st
M = (compose ((IDEA_P_F (Key,n,$1)),MESSAGES)) . m holds
len M >= 4;
A7:
m in MESSAGES
by FINSEQ_1:def 11;
A8:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
A9:
dom (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) = MESSAGES
by Th43;
A10:
rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) c= MESSAGES
by Th43;
then
rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES)) c= dom (IDEA_P ((Line (Key,(k + 1))),n))
by FUNCT_2:def 1;
then A11:
dom ((IDEA_P ((Line (Key,(k + 1))),n)) * (compose ((IDEA_P_F (Key,n,k)),MESSAGES))) = MESSAGES
by A9, RELAT_1:27;
(compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m in rng (compose ((IDEA_P_F (Key,n,k)),MESSAGES))
by A7, A9, FUNCT_1:def 3;
then reconsider M1 =
(compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m as
FinSequence of
NAT by A10, FINSEQ_1:def 11;
assume
S1[
k]
;
S1[k + 1]
then A12:
len M1 >= 4
;
let M be
FinSequence of
NAT ;
( M = (compose ((IDEA_P_F (Key,n,(k + 1))),MESSAGES)) . m implies len M >= 4 )
assume
M = (compose ((IDEA_P_F (Key,n,(k + 1))),MESSAGES)) . m
;
len M >= 4
then
M = (compose (((IDEA_P_F (Key,n,k)) ^ <*(IDEA_P ((Line (Key,(k + 1))),n))*>),MESSAGES)) . m
by Th36;
then
M = ((IDEA_P ((Line (Key,(k + 1))),n)) * (compose ((IDEA_P_F (Key,n,k)),MESSAGES))) . m
by FUNCT_7:41;
then
M = (IDEA_P ((Line (Key,(k + 1))),n)) . ((compose ((IDEA_P_F (Key,n,k)),MESSAGES)) . m)
by A7, A11, FUNCT_1:12;
hence
len M >= 4
by A12, Th42;
verum
end;
1
<= r
by A5, NAT_1:14;
then
1
- 1
<= r - 1
by XREAL_1:9;
then reconsider r1 =
r1 as
Element of
NAT by A6, INT_1:3;
dom (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) = MESSAGES
by Th43;
then A13:
(compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m in rng (compose ((IDEA_P_F (Key,n,r1)),MESSAGES))
by A4, FUNCT_1:def 3;
rng (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) c= MESSAGES
by Th43;
then reconsider M1 =
(compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m as
FinSequence of
NAT by A13, FINSEQ_1:def 11;
A14:
S1[
0 ]
proof
let M be
FinSequence of
NAT ;
( M = (compose ((IDEA_P_F (Key,n,0)),MESSAGES)) . m implies len M >= 4 )
len (IDEA_P_F (Key,n,0)) = 0
by Def17;
then A15:
IDEA_P_F (
Key,
n,
0)
= {}
;
assume
M = (compose ((IDEA_P_F (Key,n,0)),MESSAGES)) . m
;
len M >= 4
then M =
(id MESSAGES) . m
by A15, FUNCT_7:39
.=
m
by A7, FUNCT_1:18
;
hence
len M >= 4
by A2;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A14, A8);
then A16:
len M1 >= 4
;
IDEA_P_F (
Key,
n,
(r1 + 1))
= (IDEA_P_F (Key,n,r1)) ^ <*(IDEA_P ((Line (Key,(r1 + 1))),n))*>
by Th36;
then A17:
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:41;
then
m in dom ((IDEA_P ((Line (Key,r)),n)) * (compose ((IDEA_P_F (Key,n,r1)),MESSAGES)))
by A4, Th43;
then
M = (IDEA_P ((Line (Key,r)),n)) . ((compose ((IDEA_P_F (Key,n,r1)),MESSAGES)) . m)
by A1, A17, FUNCT_1:12;
hence
(
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 A16, Th42;
verum end; end;