let p, q be Element of (2 * n) -tuples_on BOOLEAN; :: thesis: ( ex L, R being sequence of (n -tuples_on BOOLEAN) st
( 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))))) ) ) & p = (IP ") . ((R . k) ^ (L . k)) ) & ex L, R being sequence of (n -tuples_on BOOLEAN) st
( 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))))) ) ) & q = (IP ") . ((R . k) ^ (L . k)) ) implies p = q )
given L1, R1 being sequence of (n -tuples_on BOOLEAN) such that A1: ( L1 . 0 = SP-Left (IP . M) & R1 . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L1 . (i + 1) = R1 . i & R1 . (i + 1) = Op-XOR ((L1 . i),(F . ((R1 . i),(RK /. (i + 1))))) ) ) & p = (IP ") . ((R1 . k) ^ (L1 . k)) ) ; :: thesis: ( for L, R being sequence of (n -tuples_on BOOLEAN) holds
( not L . 0 = SP-Left (IP . M) or not R . 0 = SP-Right (IP . M) or ex i being Nat st
( 0 <= i & i <= k - 1 & not ( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) or not q = (IP ") . ((R . k) ^ (L . k)) ) or p = q )
given L2, R2 being sequence of (n -tuples_on BOOLEAN) such that A2: ( L2 . 0 = SP-Left (IP . M) & R2 . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L2 . (i + 1) = R2 . i & R2 . (i + 1) = Op-XOR ((L2 . i),(F . ((R2 . i),(RK /. (i + 1))))) ) ) & q = (IP ") . ((R2 . k) ^ (L2 . k)) ) ; :: thesis: p = q
reconsider KD = k - 1 as Element of NAT by INT_1:3;
defpred S₁[ Nat] means ( 0 <= $1 & $1 <= k - 1 implies ( R1 . ($1 + 1) = R2 . ($1 + 1) & L1 . ($1 + 1) = L2 . ($1 + 1) ) );
A3: S₁[ 0 ]

proof

A4: L1 . (0 + 1) = R2 . 0 by A1, A2
.= L2 . (0 + 1) by A2 ;
R1 . (0 + 1) = Op-XOR ((L2 . 0),(F . ((R2 . 0),(RK /. (0 + 1))))) by A1, A2
.= R2 . (0 + 1) by A2 ;
hence S₁[ 0 ] by A4; :: thesis: verum

end;

A5: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

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

proof

assume A7: ( 0 <= i + 1 & i + 1 <= k - 1 ) ; :: thesis: ( R1 . ((i + 1) + 1) = R2 . ((i + 1) + 1) & L1 . ((i + 1) + 1) = L2 . ((i + 1) + 1) )
A8: i <= i + 1 by NAT_1:12;
A9: L1 . ((i + 1) + 1) = R2 . (i + 1) by A7, A6, A8, A1, XXREAL_0:2
.= L2 . ((i + 1) + 1) by A2, A7 ;
R1 . ((i + 1) + 1) = Op-XOR ((L1 . (i + 1)),(F . ((R1 . (i + 1)),(RK /. ((i + 1) + 1))))) by A1, A7;
hence ( R1 . ((i + 1) + 1) = R2 . ((i + 1) + 1) & L1 . ((i + 1) + 1) = L2 . ((i + 1) + 1) ) by A9, A2, A7, A6, A8, XXREAL_0:2; :: thesis: verum

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A5);
then S₁[KD] ;
hence p = q by A1, A2; :: thesis: verum