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 ;
then A7: (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by
.= p2 by FINSEQ_1:34 ;
p1 | n1 = p1 by ;
then A8: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by
.= p1 by FINSEQ_1:34 ;
((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ (p2 /^ n2) by ;
then crossover (p1,p2,n2,n1) = ((p1 | n2) ^ (p2 /^ n2)) ^ {} by
.= (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
.= p1 | n2 by ;
n1 <= len p2 by A3, A9, Def1;
then n2 <= len (p2 | n1) by ;
then A11: crossover (p1,p2,n1,n2) = (p1 | n2) ^ (((p2 | n1) /^ n2) ^ (p1 /^ n1)) by
.= ((p1 | n2) ^ ((p2 | n1) /^ n2)) ^ (p1 /^ n1) by FINSEQ_1:32 ;
len (p2 | n2) = n2 by ;
then consider i being Nat such that
A12: (len (p2 | n2)) + i = n1 by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A13: len (p1 | n2) = n2 by ;
then A14: (len (p1 | n2)) + i = n1 by ;
then i = n1 - n2 by A13;
then A15: i = n1 -' n2 by ;
A16: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ ((p2 /^ n2) | i) by
.= (p1 | n2) ^ ((p2 | n1) /^ n2) by ;
((p2 | n2) ^ (p1 /^ n2)) /^ n1 = (p1 /^ n2) /^ i by
.= p1 /^ (n2 + i) by FINSEQ_6:81
.= p1 /^ n1 by ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by ; :: 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 ;
then A19: n2 >= len p2 by ;
A20: n1 >= len p2 by ;
then p2 | n1 = p2 by FINSEQ_1:58;
then (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by
.= p2 by FINSEQ_1:34 ;
then A21: ((p2 | n1) ^ (p1 /^ n1)) /^ n2 = {} by ;
p1 | n2 = p1 by ;
then (p1 | n2) ^ (p2 /^ n2) = p1 ^ {} by
.= p1 by FINSEQ_1:34 ;
then A22: ((p1 | n2) ^ (p2 /^ n2)) | n1 = p1 by ;
p2 | n2 = p2 by ;
then (p2 | n2) ^ (p1 /^ n2) = p2 ^ {} by
.= p2 by FINSEQ_1:34 ;
then A23: ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = {} by ;
p1 | n1 = p1 by ;
then (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by
.= p1 by FINSEQ_1:34 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by ; :: 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 ; :: thesis: verum
end;
suppose n2 < len p1 ; :: thesis: n1 <= len (p1 | n2)
hence n1 <= len (p1 | n2) by ; :: 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 ;
A26: len (p1 | n1) = n1 by ;
then consider i being Nat such that
A27: (len (p1 | n1)) + i = n2 by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A28: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) ^ ((p2 /^ n1) | i) by ;
len (p2 | n1) = n1 by ;
then (len (p2 | n1)) + i = n2 by ;
then A29: crossover (p1,p2,n1,n2) = ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i) by
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i)) by FINSEQ_6:81
.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2) by ;
A30: i = n2 - n1 by ;
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 ; :: thesis: verum
end;
suppose n2 < len p2 ; :: thesis: n1 <= len (p2 | n2)
hence n1 <= len (p2 | n2) by ; :: 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 ;
hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by ; :: 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