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

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

end;

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

hence
((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1
; :: thesis: verumper cases
( n1 <= len p2 or n1 > len p2 )
;

end;

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

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;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

proof

end;

hence
crossover (p1,p2,n1,n1) = p1
by A1, RFINSEQ:8; :: thesis: verumnow :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1end;

hence
((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1
; :: thesis: verumper cases
( n1 <= len p1 or n1 > len p1 )
;

end;

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

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;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