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;
len ((p2 | n2) ^ (p1 /^ n2)) = len (crossover (p2,p1,n2)) ;
then A2: len ((p2 | n2) ^ (p1 /^ n2)) = len S by Def1;
A3: len p2 = len S by Def1;
len ((p1 | n2) ^ (p2 /^ n2)) = len (crossover (p1,p2,n2)) ;
then A4: len ((p1 | n2) ^ (p2 /^ n2)) = len S by Def1;

now :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

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 :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

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 p2 | n1 = p2 by A1, A3, FINSEQ_1:58;
then A7: (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A6, FINSEQ_5:32
.= p2 by FINSEQ_1:34 ;
p1 | n1 = p1 by A6, FINSEQ_1:58;
then A8: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A1, A3, A6, FINSEQ_5:32
.= p1 by FINSEQ_1:34 ;
((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ (p2 /^ n2) by A1, A4, A6, FINSEQ_1:58;
then crossover (p1,p2,n2,n1) = ((p1 | n2) ^ (p2 /^ n2)) ^ {} by A1, A2, A6, FINSEQ_5:32
.= (p1 | n2) ^ (p2 /^ n2) by FINSEQ_1:34 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A8, A7; :: thesis: verum

end;

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

then len (p1 | n1) = n1 by FINSEQ_1:59;
then A10: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) | n2 by A5, FINSEQ_5:22
.= p1 | n2 by A5, FINSEQ_5:77 ;
n1 <= len p2 by A3, A9, Def1;
then n2 <= len (p2 | n1) by A5, FINSEQ_1:59;
then A11: 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:32 ;
len (p2 | n2) = n2 by A1, A3, A5, A9, FINSEQ_1:59, XXREAL_0:2;
then consider i being Nat such that
A12: (len (p2 | n2)) + i = n1 by A5, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A13: len (p1 | n2) = n2 by A5, A9, FINSEQ_1:59, XXREAL_0:2;
then A14: (len (p1 | n2)) + i = n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2;
then i = n1 - n2 by A13;
then A15: i = n1 -' n2 by A5, XREAL_1:233;
A16: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ ((p2 /^ n2) | i) by A14, Th2
.= (p1 | n2) ^ ((p2 | n1) /^ n2) by A15, FINSEQ_5:80 ;
((p2 | n2) ^ (p1 /^ n2)) /^ n1 = (p1 /^ n2) /^ i by A12, FINSEQ_5:36
.= p1 /^ (n2 + i) by FINSEQ_6:81
.= p1 /^ n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A11, 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 :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

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 n2 >= len p1 by A17, XXREAL_0:2;
then A19: n2 >= len p2 by A3, Def1;
A20: n1 >= len p2 by A3, A18, Def1;
then p2 | n1 = p2 by FINSEQ_1:58;
then (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A18, FINSEQ_5:32
.= p2 by FINSEQ_1:34 ;
then A21: ((p2 | n1) ^ (p1 /^ n1)) /^ n2 = {} by A19, FINSEQ_5:32;
p1 | n2 = p1 by A17, A18, FINSEQ_1:58, XXREAL_0:2;
then (p1 | n2) ^ (p2 /^ n2) = p1 ^ {} by A19, FINSEQ_5:32
.= p1 by FINSEQ_1:34 ;
then A22: ((p1 | n2) ^ (p2 /^ n2)) | n1 = p1 by A18, FINSEQ_1:58;
p2 | n2 = p2 by A19, FINSEQ_1:58;
then (p2 | n2) ^ (p1 /^ n2) = p2 ^ {} by A17, A18, FINSEQ_5:32, XXREAL_0:2
.= p2 by FINSEQ_1:34 ;
then A23: ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = {} by A20, FINSEQ_5:32;
p1 | n1 = p1 by A18, FINSEQ_1:58;
then (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A20, FINSEQ_5:32
.= p1 by FINSEQ_1:34 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A17, A18, A21, A22, A23, FINSEQ_1:58, XXREAL_0:2; :: thesis: verum

end;

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

n1 <= len (p1 | n2)

proof

now :: thesis: n1 <= len (p1 | n2)

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:58; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then A25: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) | n1 by FINSEQ_5:22
.= p1 | n1 by A17, FINSEQ_5:77 ;
A26: len (p1 | n1) = n1 by A24, FINSEQ_1:59;
then consider i being Nat such that
A27: (len (p1 | n1)) + i = n2 by A17, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A28: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) ^ ((p2 /^ n1) | i) by A27, Th2;
len (p2 | n1) = n1 by A1, A3, A24, FINSEQ_1:59;
then (len (p2 | n1)) + i = n2 by A24, A27, FINSEQ_1:59;
then A29: crossover (p1,p2,n1,n2) = ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i) by A28, FINSEQ_5:36
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i)) by FINSEQ_6:81
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2) by A24, A27, FINSEQ_1:59 ;
A30: i = n2 - n1 by A26, A27;
n1 <= len (p2 | n2)

proof

now :: thesis: n1 <= len (p2 | n2)

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, A3, A24, FINSEQ_1:58; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = ((p2 | n2) /^ n1) ^ (p1 /^ n2) by Th1
.= ((p2 /^ n1) | (n2 -' n1)) ^ (p1 /^ n2) by FINSEQ_5:80
.= ((p2 /^ n1) | i) ^ (p1 /^ n2) by A17, A30, XREAL_1:233 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A29, A25, FINSEQ_1:32; :: thesis: verum

end;

end;

end;

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

end;

suppose A31: 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 A31; :: thesis: verum

end;

end;

end;

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