let n, m, k be non zero Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: 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 S₁[ Nat] means ( $1 <= k implies ( LB . $1 = R . (k - $1) & RB . $1 = L . (k - $1) ) );
A3: S₁[ 0 ]

proof

A4: len (R . k) = n by CARD_1:def 7;
rng IP = (2 * n) -tuples_on BOOLEAN by FUNCT_2:def 3;
then A5: (R . k) ^ (L . k) in rng IP by FINSEQ_2:131;
A6: IP . (DES-like-CoDec (M,F,IP,RK)) = (R . k) ^ (L . k) by A5, A1, FUNCT_1:35;
A7: len (R . k) = n by CARD_1:def 7;
((R . k) ^ (L . k)) | n = ((R . k) ^ (L . k)) | (dom (R . k)) by A4, FINSEQ_1:def 3
.= R . k by FINSEQ_1:21 ;
hence S₁[ 0 ] by A2, A7, A6, FINSEQ_5:37; :: thesis: verum

end;

A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: ( i + 1 <= k implies ( LB . (i + 1) = R . (k - (i + 1)) & RB . (i + 1) = L . (k - (i + 1)) ) )

assume A10: i + 1 <= k ; :: thesis: ( 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; :: thesis: verum

end;

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

end;

for i being Nat holds S₁[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; :: thesis: verum