let n be Element of NAT ; :: thesis: for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n) is Individual of S

let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,n) is Individual of S
let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,n) is Individual of S
A1: len (crossover (p1,p2,n)) = len S
proof
A2: len (crossover (p1,p2,n)) = (len (p1 | n)) + (len (p2 /^ n)) by FINSEQ_1:22;
now :: thesis: len (crossover (p1,p2,n)) = len S
per cases ( n <= len p1 or n > len p1 ) ;
suppose A3: n <= len p1 ; :: thesis: len (crossover (p1,p2,n)) = len S
len (p2 /^ n) = (len p2) -' n by RFINSEQ:29
.= (len S) -' n by Def1
.= (len p1) -' n by Def1
.= (len p1) - n by ;
then len (crossover (p1,p2,n)) = n + ((len p1) - n) by
.= len p1 ;
hence len (crossover (p1,p2,n)) = len S by Def1; :: thesis: verum
end;
suppose A4: n > len p1 ; :: thesis: len (crossover (p1,p2,n)) = len S
p1 | n = p1 | (Seg n) by FINSEQ_1:def 15;
then A5: p1 | n = p1 by ;
A6: (len p1) - n < 0 by ;
len (p2 /^ n) = (len p2) -' n by RFINSEQ:29
.= (len S) -' n by Def1
.= (len p1) -' n by Def1
.= 0 by ;
hence len (crossover (p1,p2,n)) = len S by A2, A5, Def1; :: thesis: verum
end;
end;
end;
hence len (crossover (p1,p2,n)) = len S ; :: thesis: verum
end;
for i being Element of NAT st i in dom (crossover (p1,p2,n)) holds
(crossover (p1,p2,n)) . i in S . i
proof
let i be Element of NAT ; :: thesis: ( i in dom (crossover (p1,p2,n)) implies (crossover (p1,p2,n)) . i in S . i )
assume A7: i in dom (crossover (p1,p2,n)) ; :: thesis: (crossover (p1,p2,n)) . i in S . i
now :: thesis: (crossover (p1,p2,n)) . i in S . i
per cases ( i in dom (p1 | n) or ex k being Nat st
( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) )
by ;
suppose A8: i in dom (p1 | n) ; :: thesis: (crossover (p1,p2,n)) . i in S . i
A9: dom (p1 | n) c= dom p1 by FINSEQ_5:18;
(p1 | n) . i = (p1 | n) /. i by
.= p1 /. i by
.= p1 . i by ;
then (p1 | n) . i in S . i by A8, A9, Def1;
hence (crossover (p1,p2,n)) . i in S . i by ; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) ; :: thesis: (crossover (p1,p2,n)) . i in S . i
then consider k being Nat such that
A10: k in dom (p2 /^ n) and
A11: i = (len (p1 | n)) + k ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A12: n <= len (p1 | n)
proof
n + k in dom p2 by ;
then n + k in Seg (len p2) by FINSEQ_1:def 3;
then n + k <= len p2 by FINSEQ_1:1;
then n + k <= len S by Def1;
then n + k <= len p1 by Def1;
then A13: k <= (len p1) - n by XREAL_1:19;
k in Seg (len (p2 /^ n)) by ;
then 1 <= k by FINSEQ_1:1;
then 1 <= (len p1) - n by ;
then 1 + n <= len p1 by XREAL_1:19;
then A14: n <= (len p1) - 1 by XREAL_1:19;
len p1 <= (len p1) + 1 by NAT_1:11;
then A15: (len p1) - 1 <= len p1 by XREAL_1:20;
assume n > len (p1 | n) ; :: thesis: contradiction
hence contradiction by A14, A15, FINSEQ_1:59, XXREAL_0:2; :: thesis: verum
end;
len (p1 | n) <= n by FINSEQ_5:17;
then A16: len (p1 | n) = n by ;
then n + k in Seg (len S) by ;
then n + k in Seg (len p2) by Def1;
then A17: n + k in dom p2 by FINSEQ_1:def 3;
(crossover (p1,p2,n)) . i = (p2 /^ n) . k by
.= (p2 /^ n) /. k by
.= p2 /. (n + k) by
.= p2 . (n + k) by ;
hence (crossover (p1,p2,n)) . i in S . i by ; :: thesis: verum
end;
end;
end;
hence (crossover (p1,p2,n)) . i in S . i ; :: thesis: verum
end;
hence crossover (p1,p2,n) is Individual of S by ; :: thesis: verum