defpred S₁[ Nat, Element of 28 -tuples_on BOOLEAN, Element of 28 -tuples_on BOOLEAN, Element of 28 -tuples_on BOOLEAN, Element of 28 -tuples_on BOOLEAN] means ( $4 = Op-Shift ($2,(bitshift_DES . $1)) & $5 = Op-Shift ($3,(bitshift_DES . $1)) );
A1: for i being Nat
for z, w being Element of 28 -tuples_on BOOLEAN ex z1, w1 being Element of 28 -tuples_on BOOLEAN st S₁[i,z,w,z1,w1]

proof

let i be Nat; :: thesis: for z, w being Element of 28 -tuples_on BOOLEAN ex z1, w1 being Element of 28 -tuples_on BOOLEAN st S₁[i,z,w,z1,w1]
let z, w be Element of 28 -tuples_on BOOLEAN; :: thesis: ex z1, w1 being Element of 28 -tuples_on BOOLEAN st S₁[i,z,w,z1,w1]
reconsider z1 = Op-Shift (z,(bitshift_DES . i)) as Element of 28 -tuples_on BOOLEAN by Th14;
reconsider w1 = Op-Shift (w,(bitshift_DES . i)) as Element of 28 -tuples_on BOOLEAN by Th14;
take z1 ; :: thesis: ex w1 being Element of 28 -tuples_on BOOLEAN st S₁[i,z,w,z1,w1]
take w1 ; :: thesis: S₁[i,z,w,z1,w1]
thus S₁[i,z,w,z1,w1] ; :: thesis: verum

end;

reconsider C0 = Op-Left ((DES-PC1 Key),28) as Element of 28 -tuples_on BOOLEAN by Th1;
( DES-PC1 Key is Element of 56 -tuples_on BOOLEAN & 28 <= 56 & 28 = 56 - 28 ) ;
then reconsider D0 = Op-Right ((DES-PC1 Key),28) as Element of 28 -tuples_on BOOLEAN by Th2;
consider C, D being sequence of (28 -tuples_on BOOLEAN) such that
A2: ( C . 0 = C0 & D . 0 = D0 & ( for n being Nat holds S₁[n,C . n,D . n,C . (n + 1),D . (n + 1)] ) ) from RECDEF_2:sch 3(A1);
defpred S₂[ Nat, set ] means $2 = DES-PC2 ((C . $1) ^ (D . $1));
A3: for k being Nat st k in Seg 16 holds
ex x being Element of 48 -tuples_on BOOLEAN st S₂[k,x] ;
consider OUT being FinSequence of 48 -tuples_on BOOLEAN such that
A4: ( dom OUT = Seg 16 & ( for j being Nat st j in Seg 16 holds
S₂[j,OUT . j] ) ) from FINSEQ_1:sch 5(A3);
len OUT = 16 by A4, FINSEQ_1:def 3;
then reconsider OUT = OUT as Element of 16 -tuples_on (48 -tuples_on BOOLEAN) by FINSEQ_2:92;

A5: now :: thesis: for i being Element of NAT st 0 <= i & i <= 15 holds
( OUT . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) )

let i be Element of NAT ; :: thesis: ( 0 <= i & i <= 15 implies ( OUT . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) )
assume A6: ( 0 <= i & i <= 15 ) ; :: thesis: ( OUT . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) )
A7: 0 + 1 <= i + 1 by XREAL_1:6;
i + 1 <= 15 + 1 by A6, XREAL_1:6;
then i + 1 in Seg 16 by A7;
hence ( OUT . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) by A2, A4; :: thesis: verum

end;

thus ex b₁ being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₁ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) by A5, A2; :: thesis: verum