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

(crossover (p1,p2,n)) . i in S . i

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

for i being Element of NAT st i in dom (crossover (p1,p2,n)) holds
A2:
len (crossover (p1,p2,n)) = (len (p1 | n)) + (len (p2 /^ n))
by FINSEQ_1:22;

end;now :: thesis: len (crossover (p1,p2,n)) = len Send;

hence
len (crossover (p1,p2,n)) = len S
; :: thesis: verumper cases
( n <= len p1 or n > len p1 )
;

end;

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 A3, XREAL_1:233 ;

then len (crossover (p1,p2,n)) = n + ((len p1) - n) by A2, A3, FINSEQ_1:59

.= len p1 ;

hence len (crossover (p1,p2,n)) = len S by Def1; :: thesis: verum

end;.= (len S) -' n by Def1

.= (len p1) -' n by Def1

.= (len p1) - n by A3, XREAL_1:233 ;

then len (crossover (p1,p2,n)) = n + ((len p1) - n) by A2, A3, FINSEQ_1:59

.= len p1 ;

hence len (crossover (p1,p2,n)) = len S by Def1; :: thesis: verum

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 A4, FINSEQ_2:20;

A6: (len p1) - n < 0 by A4, XREAL_1:49;

len (p2 /^ n) = (len p2) -' n by RFINSEQ:29

.= (len S) -' n by Def1

.= (len p1) -' n by Def1

.= 0 by A6, XREAL_0:def 2 ;

hence len (crossover (p1,p2,n)) = len S by A2, A5, Def1; :: thesis: verum

end;then A5: p1 | n = p1 by A4, FINSEQ_2:20;

A6: (len p1) - n < 0 by A4, XREAL_1:49;

len (p2 /^ n) = (len p2) -' n by RFINSEQ:29

.= (len S) -' n by Def1

.= (len p1) -' n by Def1

.= 0 by A6, XREAL_0:def 2 ;

hence len (crossover (p1,p2,n)) = len S by A2, A5, Def1; :: thesis: verum

(crossover (p1,p2,n)) . i in S . i

proof

hence
crossover (p1,p2,n) is Individual of S
by A1, Def1; :: thesis: verum
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

end;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 . iend;

hence
(crossover (p1,p2,n)) . i in S . i
; :: thesis: verumper cases
( i in dom (p1 | n) or ex k being Nat st

( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) ) by A7, FINSEQ_1:25;

end;

( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) ) by A7, FINSEQ_1:25;

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 A8, PARTFUN1:def 6

.= p1 /. i by A8, FINSEQ_4:70

.= p1 . i by A8, A9, PARTFUN1:def 6 ;

then (p1 | n) . i in S . i by A8, A9, Def1;

hence (crossover (p1,p2,n)) . i in S . i by A8, FINSEQ_1:def 7; :: thesis: verum

end;(p1 | n) . i = (p1 | n) /. i by A8, PARTFUN1:def 6

.= p1 /. i by A8, FINSEQ_4:70

.= p1 . i by A8, A9, PARTFUN1:def 6 ;

then (p1 | n) . i in S . i by A8, A9, Def1;

hence (crossover (p1,p2,n)) . i in S . i by A8, FINSEQ_1:def 7; :: thesis: verum

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

( 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)

then A16: len (p1 | n) = n by A12, XXREAL_0:1;

then n + k in Seg (len S) by A1, A7, A11, FINSEQ_1:def 3;

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 A10, A11, FINSEQ_1:def 7

.= (p2 /^ n) /. k by A10, PARTFUN1:def 6

.= p2 /. (n + k) by A10, FINSEQ_5:27

.= p2 . (n + k) by A17, PARTFUN1:def 6 ;

hence (crossover (p1,p2,n)) . i in S . i by A11, A16, A17, Def1; :: thesis: verum

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

len (p1 | n) <= n
by FINSEQ_5:17;
n + k in dom p2
by A10, FINSEQ_5:26;

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 A10, FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then 1 <= (len p1) - n by A13, XXREAL_0:2;

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;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 A10, FINSEQ_1:def 3;

then 1 <= k by FINSEQ_1:1;

then 1 <= (len p1) - n by A13, XXREAL_0:2;

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

then A16: len (p1 | n) = n by A12, XXREAL_0:1;

then n + k in Seg (len S) by A1, A7, A11, FINSEQ_1:def 3;

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 A10, A11, FINSEQ_1:def 7

.= (p2 /^ n) /. k by A10, PARTFUN1:def 6

.= p2 /. (n + k) by A10, FINSEQ_5:27

.= p2 . (n + k) by A17, PARTFUN1:def 6 ;

hence (crossover (p1,p2,n)) . i in S . i by A11, A16, A17, Def1; :: thesis: verum