let n, m, k be non zero Element of NAT ; for RK being Element of k -tuples_on (m -tuples_on BOOLEAN)
for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN holds DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let RK be Element of k -tuples_on (m -tuples_on BOOLEAN); for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN holds DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let F be Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN); for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN holds DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let IP be Permutation of ((2 * n) -tuples_on BOOLEAN); for M being Element of (2 * n) -tuples_on BOOLEAN holds DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let M be Element of (2 * n) -tuples_on BOOLEAN; DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
set REVRKS = Rev RK;
set EM = DES-like-CoDec (M,F,IP,RK);
consider L, R being sequence of (n -tuples_on BOOLEAN) such that
A1:
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & DES-like-CoDec (M,F,IP,RK) = (IP ") . ((R . k) ^ (L . k)) )
by Def29;
consider LB, RB being sequence of (n -tuples_on BOOLEAN) such that
A2:
( LB . 0 = SP-Left (IP . (DES-like-CoDec (M,F,IP,RK))) & RB . 0 = SP-Right (IP . (DES-like-CoDec (M,F,IP,RK))) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( LB . (i + 1) = RB . i & RB . (i + 1) = Op-XOR ((LB . i),(F . ((RB . i),((Rev RK) /. (i + 1))))) ) ) & DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = (IP ") . ((RB . k) ^ (LB . k)) )
by Def29;
defpred S1[ Nat] means ( $1 <= k implies ( LB . $1 = R . (k - $1) & RB . $1 = L . (k - $1) ) );
A3:
S1[ 0 ]
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A9:
S1[
i]
;
S1[i + 1]
now ( i + 1 <= k implies ( LB . (i + 1) = R . (k - (i + 1)) & RB . (i + 1) = L . (k - (i + 1)) ) )assume A10:
i + 1
<= k
;
( LB . (i + 1) = R . (k - (i + 1)) & RB . (i + 1) = L . (k - (i + 1)) )A11:
i <= i + 1
by NAT_1:11;
then A12:
i <= k
by A10, XXREAL_0:2;
A13:
(i + 1) - (i + 1) <= k - (i + 1)
by A10, XREAL_1:9;
A14:
(k - 1) - i <= (k - 1) - 0
by XREAL_1:13;
i - i <= k - i
by A12, XREAL_1:9;
then reconsider i16 =
k - i as
Element of
NAT by INT_1:3;
reconsider i161 =
k - (i + 1) as
Element of
NAT by A13, INT_1:3;
A15:
(i + 1) - 1
<= k - 1
by A10, XREAL_1:9;
then A16:
(
LB . (i + 1) = RB . i &
RB . (i + 1) = Op-XOR (
(LB . i),
(F . ((RB . i),((Rev RK) /. (i + 1))))) )
by A2;
reconsider Ki =
(Rev RK) /. (i + 1) as
Element of
m -tuples_on BOOLEAN ;
A17:
RB . i =
L . ((k - (i + 1)) + 1)
by A9, A10, A11, XXREAL_0:2
.=
R . i161
by A1, A14
;
A18:
len RK = k
by CARD_1:def 7;
( 1
<= i + 1 &
i + 1
<= k )
by A10, NAT_1:11;
then
i + 1
in Seg k
;
then A19:
i + 1
in dom RK
by A18, FINSEQ_1:def 3;
then A20:
i + 1
in dom (Rev RK)
by FINSEQ_5:57;
A21:
k - i <= k - 0
by XREAL_1:10;
k - (k - 1) <= k - i
by A15, XREAL_1:10;
then
i16 in Seg k
by A21;
then A22:
k - i in dom RK
by A18, FINSEQ_1:def 3;
A23:
(Rev RK) /. (i + 1) =
(Rev RK) . (i + 1)
by A20, PARTFUN1:def 6
.=
RK . (((len RK) - (i + 1)) + 1)
by A19, FINSEQ_5:58
.=
RK /. (k - i)
by A22, A18, PARTFUN1:def 6
;
LB . i =
Op-XOR (
(L . i161),
(F . ((R . i161),(RK /. (i161 + 1)))))
by A1, A14, A9, A10, A11, XXREAL_0:2
.=
Op-XOR (
(L . i161),
(F . ((R . i161),Ki)))
by A23
;
hence
(
LB . (i + 1) = R . (k - (i + 1)) &
RB . (i + 1) = L . (k - (i + 1)) )
by A16, A17, Th17;
verum end;
hence
S1[
i + 1]
;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A3, A8);
then
( LB . k = R . (k - k) & RB . k = L . (k - k) )
;
then
(RB . k) ^ (LB . k) = IP . M
by Th3, A1;
hence
DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
by A2, FUNCT_2:26; verum