let n1, n2 be Element of NAT ; :: thesis: for S being Gene-Set
for p1, p2 being Individual of S holds crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1
let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1
let p1, p2 be Individual of S; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1
A1: len p1 = len S by Def1;
A2: len p2 = len S by Def1;
len ((p1 | n2) ^ (p2 /^ n2)) = len (crossover p1,p2,n2) ;
then A3: len ((p1 | n2) ^ (p2 /^ n2)) = len S by Def1;
len ((p2 | n2) ^ (p1 /^ n2)) = len (crossover p2,p1,n2) ;
then A4: len ((p2 | n2) ^ (p1 /^ n2)) = len S by Def1;

now

per cases ( ( n1 >= n2 & n2 > 0 ) or ( n1 < n2 & n2 > 0 ) or n2 = 0 ) by NAT_1:3;

suppose A5: ( n1 >= n2 & n2 > 0 ) ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

now

per cases ( n1 >= len p1 or n1 < len p1 ) ;

suppose A6: n1 >= len p1 ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

then p1 | n1 = p1 by FINSEQ_1:79;
then A7: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A1, A2, A6, FINSEQ_5:35
.= p1 by FINSEQ_1:47 ;
p2 | n1 = p2 by A1, A2, A6, FINSEQ_1:79;
then A8: (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A6, FINSEQ_5:35
.= p2 by FINSEQ_1:47 ;
((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ (p2 /^ n2) by A1, A3, A6, FINSEQ_1:79;
then crossover p1,p2,n2,n1 = ((p1 | n2) ^ (p2 /^ n2)) ^ {} by A1, A4, A6, FINSEQ_5:35
.= (p1 | n2) ^ (p2 /^ n2) by FINSEQ_1:47 ;
hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 by A7, A8; :: thesis: verum

end;

suppose A9: n1 < len p1 ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

then n1 <= len p2 by A2, Def1;
then A10: n2 <= len (p2 | n1) by A5, FINSEQ_1:80;
len (p2 | n2) = n2 by A1, A2, A5, A9, FINSEQ_1:80, XXREAL_0:2;
then consider i being Nat such that
A11: (len (p2 | n2)) + i = n1 by A5, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A12: len (p1 | n2) = n2 by A5, A9, FINSEQ_1:80, XXREAL_0:2;
then A13: (len (p1 | n2)) + i = n1 by A1, A2, A5, A9, A11, FINSEQ_1:80, XXREAL_0:2;
then i = n1 - n2 by A12;
then A14: i = n1 -' n2 by A5, XREAL_1:235;
len (p1 | n1) = n1 by A9, FINSEQ_1:80;
then ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) | n2 by A5, FINSEQ_5:25
.= p1 | n2 by A5, FINSEQ_5:80 ;
then A15: crossover p1,p2,n1,n2 = (p1 | n2) ^ (((p2 | n1) /^ n2) ^ (p1 /^ n1)) by A10, Th1
.= ((p1 | n2) ^ ((p2 | n1) /^ n2)) ^ (p1 /^ n1) by FINSEQ_1:45 ;
A16: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ ((p2 /^ n2) | i) by A13, Th2
.= (p1 | n2) ^ ((p2 | n1) /^ n2) by A14, FINSEQ_5:83 ;
((p2 | n2) ^ (p1 /^ n2)) /^ n1 = (p1 /^ n2) /^ i by A11, FINSEQ_5:39
.= p1 /^ (n2 + i) by FINSEQ_6:87
.= p1 /^ n1 by A1, A2, A5, A9, A11, FINSEQ_1:80, XXREAL_0:2 ;
hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 by A15, A16; :: thesis: verum

end;

end;

end;

hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 ; :: thesis: verum

end;

suppose A17: ( n1 < n2 & n2 > 0 ) ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

now

per cases ( n1 >= len p1 or n1 < len p1 ) ;

suppose A18: n1 >= len p1 ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

then A19: n1 >= len p2 by A2, Def1;
n2 >= len p1 by A17, A18, XXREAL_0:2;
then A20: n2 >= len p2 by A2, Def1;
p1 | n1 = p1 by A18, FINSEQ_1:79;
then A21: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A19, FINSEQ_5:35
.= p1 by FINSEQ_1:47 ;
p2 | n1 = p2 by A19, FINSEQ_1:79;
then (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A18, FINSEQ_5:35
.= p2 by FINSEQ_1:47 ;
then A22: ((p2 | n1) ^ (p1 /^ n1)) /^ n2 = {} by A20, FINSEQ_5:35;
p1 | n2 = p1 by A17, A18, FINSEQ_1:79, XXREAL_0:2;
then (p1 | n2) ^ (p2 /^ n2) = p1 ^ {} by A20, FINSEQ_5:35
.= p1 by FINSEQ_1:47 ;
then A23: ((p1 | n2) ^ (p2 /^ n2)) | n1 = p1 by A18, FINSEQ_1:79;
p2 | n2 = p2 by A20, FINSEQ_1:79;
then (p2 | n2) ^ (p1 /^ n2) = p2 ^ {} by A17, A18, FINSEQ_5:35, XXREAL_0:2
.= p2 by FINSEQ_1:47 ;
then ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = {} by A19, FINSEQ_5:35;
hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 by A17, A18, A21, A22, A23, FINSEQ_1:79, XXREAL_0:2; :: thesis: verum

end;

suppose A24: n1 < len p1 ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

then A25: len (p1 | n1) = n1 by FINSEQ_1:80;
A26: len (p2 | n1) = n1 by A1, A2, A24, FINSEQ_1:80;
consider i being Nat such that
A27: (len (p1 | n1)) + i = n2 by A17, A25, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A28: (len (p2 | n1)) + i = n2 by A24, A26, A27, FINSEQ_1:80;
A29: n1 <= len (p1 | n2)

proof

now

per cases ( n2 >= len p1 or n2 < len p1 ) ;

suppose n2 >= len p1 ; :: thesis: n1 <= len (p1 | n2)

hence n1 <= len (p1 | n2) by A24, FINSEQ_1:79; :: thesis: verum

end;

suppose n2 < len p1 ; :: thesis: n1 <= len (p1 | n2)

hence n1 <= len (p1 | n2) by A17, FINSEQ_1:80; :: thesis: verum

end;

end;

end;

hence n1 <= len (p1 | n2) ; :: thesis: verum

end;

A30: n1 <= len (p2 | n2)

proof

now

per cases ( n2 >= len p2 or n2 < len p2 ) ;

suppose n2 >= len p2 ; :: thesis: n1 <= len (p2 | n2)

hence n1 <= len (p2 | n2) by A1, A2, A24, FINSEQ_1:79; :: thesis: verum

end;

suppose n2 < len p2 ; :: thesis: n1 <= len (p2 | n2)

hence n1 <= len (p2 | n2) by A17, FINSEQ_1:80; :: thesis: verum

end;

end;

end;

hence n1 <= len (p2 | n2) ; :: thesis: verum

end;

A31: i = n2 - n1 by A25, A27;
((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) ^ ((p2 /^ n1) | i) by A27, Th2;
then A32: crossover p1,p2,n1,n2 = ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i) by A28, FINSEQ_5:39
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i)) by FINSEQ_6:87
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2) by A24, A27, FINSEQ_1:80 ;
A33: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) | n1 by A29, FINSEQ_5:25
.= p1 | n1 by A17, FINSEQ_5:80 ;
((p2 | n2) ^ (p1 /^ n2)) /^ n1 = ((p2 | n2) /^ n1) ^ (p1 /^ n2) by A30, Th1
.= ((p2 /^ n1) | (n2 -' n1)) ^ (p1 /^ n2) by FINSEQ_5:83
.= ((p2 /^ n1) | i) ^ (p1 /^ n2) by A17, A31, XREAL_1:235 ;
hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 by A32, A33, FINSEQ_1:45; :: thesis: verum

end;

end;

end;

hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 ; :: thesis: verum

end;

suppose A34: n2 = 0 ; :: thesis: crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1

then crossover p1,p2,n1,n2 = crossover p2,p1,n1 by Th8
.= crossover p1,p2,0 ,n1 by Th7 ;
hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 by A34; :: thesis: verum

end;

end;

end;

hence crossover p1,p2,n1,n2 = crossover p1,p2,n2,n1 ; :: thesis: verum