let n1 be Element of NAT ; :: thesis: for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n1,n1) = p1
let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,n1,n1) = p1
let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,n1,n1) = p1
A1: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1

proof

now :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1

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

suppose n1 <= len p2 ; :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1

then len (p2 | n1) = n1 by FINSEQ_1:59;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 by FINSEQ_5:37; :: thesis: verum

end;

suppose n1 > len p2 ; :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1

then A2: n1 > len S by Def1;
then n1 > len (crossover (p2,p1,n1)) by Def1;
then A3: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = {} by FINSEQ_5:32;
n1 > len p1 by A2, Def1;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 by A3, FINSEQ_5:32; :: thesis: verum

end;

end;

end;

hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 ; :: thesis: verum

end;

((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1

proof

now :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1

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

suppose n1 <= len p1 ; :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1

then len (p1 | n1) = n1 by FINSEQ_1:59;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 by FINSEQ_5:23; :: thesis: verum

end;

suppose A4: n1 > len p1 ; :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1

then A5: n1 > len S by Def1;
then A6: n1 > len p2 by Def1;
n1 > len (crossover (p1,p2,n1)) by A5, Def1;
then ((p1 | n1) ^ (p2 /^ n1)) | n1 = (p1 | n1) ^ (p2 /^ n1) by FINSEQ_1:58
.= p1 ^ (p2 /^ n1) by A4, FINSEQ_1:58
.= p1 ^ {} by A6, FINSEQ_5:32
.= p1 by FINSEQ_1:34
.= p1 | n1 by A4, FINSEQ_1:58 ;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 ; :: thesis: verum

end;

end;

end;

hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 ; :: thesis: verum

end;

hence crossover (p1,p2,n1,n1) = p1 by A1, RFINSEQ:8; :: thesis: verum