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: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1

proof

now

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:80;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 by FINSEQ_5:26; :: thesis: verum

end;

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

then A3: n1 > len S by Def1;
then A4: n1 > len p2 by Def1;
n1 > len (crossover p1,p2,n1) by A3, Def1;
then ((p1 | n1) ^ (p2 /^ n1)) | n1 = (p1 | n1) ^ (p2 /^ n1) by FINSEQ_1:79
.= p1 ^ (p2 /^ n1) by A2, FINSEQ_1:79
.= p1 ^ {} by A4, FINSEQ_5:35
.= p1 by FINSEQ_1:47
.= p1 | n1 by A2, FINSEQ_1:79 ;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 ; :: thesis: verum

end;

end;

end;

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

end;

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

proof

now

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:80;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 by FINSEQ_5:40; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence crossover p1,p2,n1,n1 = p1 by A1, RFINSEQ:21; :: thesis: verum