let n, m, k be non empty Element of NAT ; :: thesis:
let RK be Element of k -tuples_on (m -tuples_on BOOLEAN); :: thesis:
let F be Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN); :: thesis:
let IP be Permutation of ((2 * n) -tuples_on BOOLEAN); :: thesis:
let M be Element of (2 * n) -tuples_on BOOLEAN; :: thesis:
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
P1: ( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Element of 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 defOPDESlike;
consider LB, RB being sequence of (n -tuples_on BOOLEAN) such that
P2: ( 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 Element of 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 defOPDESlike;
defpred S₁[ Nat] means ( $1 <= k implies ( LB . $1 = R . (k - $1) & RB . $1 = L . (k - $1) ) );
PN0: S₁[ 0 ]

proof

Q1: len (R . k) = n by CARD_1:def 7;
rng IP = (2 * n) -tuples_on BOOLEAN by FUNCT_2:def 3;
then X2: (R . k) ^ (L . k) in rng IP by FINSEQ_2:131;
LIPEM: IP . (DES-like-CoDec (M,F,IP,RK)) = (R . k) ^ (L . k) by X2, P1, FUNCT_1:35;
ATLK: len (R . k) = n by CARD_1:def 7;
((R . k) ^ (L . k)) | n = ((R . k) ^ (L . k)) | (dom (R . k)) by Q1, FINSEQ_1:def 3
.= R . k by FINSEQ_1:21 ;
hence S₁[ 0 ] by P2, ATLK, LIPEM, FINSEQ_5:37; :: thesis:

end;

PN1: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis:
assume PN11: S₁[i] ; :: thesis:

now :: thesis:

assume PN12: i + 1 <= k ; :: thesis:
PN13P: i <= i + 1 by NAT_1:11;
then PN13: i <= k by PN12, XXREAL_0:2;
XX0: (i + 1) - (i + 1) <= k - (i + 1) by PN12, XREAL_1:9;
IX1P: (k - 1) - i <= (k - 1) - 0 by XREAL_1:13;
i - i <= k - i by PN13, 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 XX0, INT_1:3;
PN15: (i + 1) - 1 <= k - 1 by PN12, XREAL_1:9;
then PN16: ( LB . (i + 1) = RB . i & RB . (i + 1) = Op-XOR ((LB . i),(F . ((RB . i),((Rev RK) /. (i + 1))))) ) by P2;
reconsider Ki = (Rev RK) /. (i + 1) as Element of m -tuples_on BOOLEAN ;
Y1: RB . i = L . ((k - (i + 1)) + 1) by PN11, PN12, PN13P, XXREAL_0:2
.= R . i161 by P1, IX1P ;
Y12: len RK = k by CARD_1:def 7;
( 1 <= i + 1 & i + 1 <= k ) by PN12, NAT_1:11;
then i + 1 in Seg k ;
then Y10: i + 1 in dom RK by Y12, FINSEQ_1:def 3;
then Y11: i + 1 in dom (Rev RK) by FINSEQ_5:57;
Y130: k - i <= k - 0 by XREAL_1:10;
k - (k - 1) <= k - i by PN15, XREAL_1:10;
then i16 in Seg k by Y130;
then Y13: k - i in dom RK by Y12, FINSEQ_1:def 3;
Y2: (Rev RK) /. (i + 1) = (Rev RK) . (i + 1) by Y11, PARTFUN1:def 6
.= RK . (((len RK) - (i + 1)) + 1) by Y10, FINSEQ_5:58
.= RK /. (k - i) by Y13, Y12, PARTFUN1:def 6 ;
LB . i = Op-XOR ((L . i161),(F . ((R . i161),(RK /. (i161 + 1))))) by P1, IX1P, PN11, PN12, PN13P, XXREAL_0:2
.= Op-XOR ((L . i161),(F . ((R . i161),Ki))) by Y2 ;
hence ( LB . (i + 1) = R . (k - (i + 1)) & RB . (i + 1) = L . (k - (i + 1)) ) by PN16, Y1, LM011; :: thesis:

end;

hence S₁[i + 1] ; :: thesis:

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(PN0, PN1);
then ( LB . k = R . (k - k) & RB . k = L . (k - k) ) ;
then (RB . k) ^ (LB . k) = IP . M by SPLR, P1;
hence DES-like-CoDec ((DES-like-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M by P2, FUNCT_2:26; :: thesis: