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 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))))) ) ) & 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 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))))) ) ) & q = (IP ") . ((R . k) ^ (L . k)) ) implies p = q )
given L1, R1 being sequence of (n -tuples_on BOOLEAN) such that A3: ( L1 . 0 = SP-Left (IP . M) & R1 . 0 = SP-Right (IP . M) & ( for i being Element of 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 Element of 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 A4: ( L2 . 0 = SP-Left (IP . M) & R2 . 0 = SP-Right (IP . M) & ( for i being Element of 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
0 + 1 <= k by INT_1:7;
then TK: 1 - 1 <= k - 1 by XREAL_1:9;
then reconsider KD = k - 1 as Element of NAT by INT_1:3;
defpred S₁[ Element of NAT ] means ( 0 <= $1 & $1 <= k - 1 implies ( R1 . ($1 + 1) = R2 . ($1 + 1) & L1 . ($1 + 1) = L2 . ($1 + 1) ) );
P0: S₁[ 0 ]

proof

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

end;

P1: now :: thesis: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume P11: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume P12: ( 0 <= i + 1 & i + 1 <= k - 1 ) ; :: thesis: ( R1 . ((i + 1) + 1) = R2 . ((i + 1) + 1) & L1 . ((i + 1) + 1) = L2 . ((i + 1) + 1) )
P14P: i <= i + 1 by NAT_1:12;
Q1: L1 . ((i + 1) + 1) = R2 . (i + 1) by P12, P11, P14P, A3, XXREAL_0:2
.= L2 . ((i + 1) + 1) by A4, P12 ;
R1 . ((i + 1) + 1) = Op-XOR ((L1 . (i + 1)),(F . ((R1 . (i + 1)),(RK /. ((i + 1) + 1))))) by A3, P12;
hence ( R1 . ((i + 1) + 1) = R2 . ((i + 1) + 1) & L1 . ((i + 1) + 1) = L2 . ((i + 1) + 1) ) by Q1, A4, P12, P11, P14P, XXREAL_0:2; :: thesis: verum

end;

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(P0, P1);
then S₁[KD] ;
hence p = q by A3, A4; :: thesis: verum