let n1, n2 be Element of NAT ; :: thesis: for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

A1: len p1 = len S by Def1;

len ((p2 | n2) ^ (p1 /^ n2)) = len (crossover (p2,p1,n2)) ;

then A2: len ((p2 | n2) ^ (p1 /^ n2)) = len S by Def1;

A3: len p2 = len S by Def1;

len ((p1 | n2) ^ (p2 /^ n2)) = len (crossover (p1,p2,n2)) ;

then A4: len ((p1 | n2) ^ (p2 /^ n2)) = len S by Def1;

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

A1: len p1 = len S by Def1;

len ((p2 | n2) ^ (p1 /^ n2)) = len (crossover (p2,p1,n2)) ;

then A2: len ((p2 | n2) ^ (p1 /^ n2)) = len S by Def1;

A3: len p2 = len S by Def1;

len ((p1 | n2) ^ (p2 /^ n2)) = len (crossover (p1,p2,n2)) ;

then A4: len ((p1 | n2) ^ (p2 /^ n2)) = len S by Def1;

now :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)end;

hence
crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)
; :: thesis: verumper cases
( ( n1 >= n2 & n2 > 0 ) or ( n1 < n2 & n2 > 0 ) or n2 = 0 )
by NAT_1:3;

end;

suppose A5:
( n1 >= n2 & n2 > 0 )
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

end;

now :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)end;

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

end;

suppose A6:
n1 >= len p1
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

then
p2 | n1 = p2
by A1, A3, FINSEQ_1:58;

then A7: (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A6, FINSEQ_5:32

.= p2 by FINSEQ_1:34 ;

p1 | n1 = p1 by A6, FINSEQ_1:58;

then A8: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A1, A3, A6, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ (p2 /^ n2) by A1, A4, A6, FINSEQ_1:58;

then crossover (p1,p2,n2,n1) = ((p1 | n2) ^ (p2 /^ n2)) ^ {} by A1, A2, A6, FINSEQ_5:32

.= (p1 | n2) ^ (p2 /^ n2) by FINSEQ_1:34 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A8, A7; :: thesis: verum

end;then A7: (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A6, FINSEQ_5:32

.= p2 by FINSEQ_1:34 ;

p1 | n1 = p1 by A6, FINSEQ_1:58;

then A8: (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A1, A3, A6, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ (p2 /^ n2) by A1, A4, A6, FINSEQ_1:58;

then crossover (p1,p2,n2,n1) = ((p1 | n2) ^ (p2 /^ n2)) ^ {} by A1, A2, A6, FINSEQ_5:32

.= (p1 | n2) ^ (p2 /^ n2) by FINSEQ_1:34 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A8, A7; :: thesis: verum

suppose A9:
n1 < len p1
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

then
len (p1 | n1) = n1
by FINSEQ_1:59;

then A10: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) | n2 by A5, FINSEQ_5:22

.= p1 | n2 by A5, FINSEQ_5:77 ;

n1 <= len p2 by A3, A9, Def1;

then n2 <= len (p2 | n1) by A5, FINSEQ_1:59;

then A11: crossover (p1,p2,n1,n2) = (p1 | n2) ^ (((p2 | n1) /^ n2) ^ (p1 /^ n1)) by A10, Th1

.= ((p1 | n2) ^ ((p2 | n1) /^ n2)) ^ (p1 /^ n1) by FINSEQ_1:32 ;

len (p2 | n2) = n2 by A1, A3, A5, A9, FINSEQ_1:59, XXREAL_0:2;

then consider i being Nat such that

A12: (len (p2 | n2)) + i = n1 by A5, NAT_1:10;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

A13: len (p1 | n2) = n2 by A5, A9, FINSEQ_1:59, XXREAL_0:2;

then A14: (len (p1 | n2)) + i = n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2;

then i = n1 - n2 by A13;

then A15: i = n1 -' n2 by A5, XREAL_1:233;

A16: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ ((p2 /^ n2) | i) by A14, Th2

.= (p1 | n2) ^ ((p2 | n1) /^ n2) by A15, FINSEQ_5:80 ;

((p2 | n2) ^ (p1 /^ n2)) /^ n1 = (p1 /^ n2) /^ i by A12, FINSEQ_5:36

.= p1 /^ (n2 + i) by FINSEQ_6:81

.= p1 /^ n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A11, A16; :: thesis: verum

end;then A10: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) | n2 by A5, FINSEQ_5:22

.= p1 | n2 by A5, FINSEQ_5:77 ;

n1 <= len p2 by A3, A9, Def1;

then n2 <= len (p2 | n1) by A5, FINSEQ_1:59;

then A11: crossover (p1,p2,n1,n2) = (p1 | n2) ^ (((p2 | n1) /^ n2) ^ (p1 /^ n1)) by A10, Th1

.= ((p1 | n2) ^ ((p2 | n1) /^ n2)) ^ (p1 /^ n1) by FINSEQ_1:32 ;

len (p2 | n2) = n2 by A1, A3, A5, A9, FINSEQ_1:59, XXREAL_0:2;

then consider i being Nat such that

A12: (len (p2 | n2)) + i = n1 by A5, NAT_1:10;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

A13: len (p1 | n2) = n2 by A5, A9, FINSEQ_1:59, XXREAL_0:2;

then A14: (len (p1 | n2)) + i = n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2;

then i = n1 - n2 by A13;

then A15: i = n1 -' n2 by A5, XREAL_1:233;

A16: ((p1 | n2) ^ (p2 /^ n2)) | n1 = (p1 | n2) ^ ((p2 /^ n2) | i) by A14, Th2

.= (p1 | n2) ^ ((p2 | n1) /^ n2) by A15, FINSEQ_5:80 ;

((p2 | n2) ^ (p1 /^ n2)) /^ n1 = (p1 /^ n2) /^ i by A12, FINSEQ_5:36

.= p1 /^ (n2 + i) by FINSEQ_6:81

.= p1 /^ n1 by A1, A3, A5, A9, A12, FINSEQ_1:59, XXREAL_0:2 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A11, A16; :: thesis: verum

suppose A17:
( n1 < n2 & n2 > 0 )
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

end;

now :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)end;

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

end;

suppose A18:
n1 >= len p1
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

then
n2 >= len p1
by A17, XXREAL_0:2;

then A19: n2 >= len p2 by A3, Def1;

A20: n1 >= len p2 by A3, A18, Def1;

then p2 | n1 = p2 by FINSEQ_1:58;

then (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A18, FINSEQ_5:32

.= p2 by FINSEQ_1:34 ;

then A21: ((p2 | n1) ^ (p1 /^ n1)) /^ n2 = {} by A19, FINSEQ_5:32;

p1 | n2 = p1 by A17, A18, FINSEQ_1:58, XXREAL_0:2;

then (p1 | n2) ^ (p2 /^ n2) = p1 ^ {} by A19, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

then A22: ((p1 | n2) ^ (p2 /^ n2)) | n1 = p1 by A18, FINSEQ_1:58;

p2 | n2 = p2 by A19, FINSEQ_1:58;

then (p2 | n2) ^ (p1 /^ n2) = p2 ^ {} by A17, A18, FINSEQ_5:32, XXREAL_0:2

.= p2 by FINSEQ_1:34 ;

then A23: ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = {} by A20, FINSEQ_5:32;

p1 | n1 = p1 by A18, FINSEQ_1:58;

then (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A20, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A17, A18, A21, A22, A23, FINSEQ_1:58, XXREAL_0:2; :: thesis: verum

end;then A19: n2 >= len p2 by A3, Def1;

A20: n1 >= len p2 by A3, A18, Def1;

then p2 | n1 = p2 by FINSEQ_1:58;

then (p2 | n1) ^ (p1 /^ n1) = p2 ^ {} by A18, FINSEQ_5:32

.= p2 by FINSEQ_1:34 ;

then A21: ((p2 | n1) ^ (p1 /^ n1)) /^ n2 = {} by A19, FINSEQ_5:32;

p1 | n2 = p1 by A17, A18, FINSEQ_1:58, XXREAL_0:2;

then (p1 | n2) ^ (p2 /^ n2) = p1 ^ {} by A19, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

then A22: ((p1 | n2) ^ (p2 /^ n2)) | n1 = p1 by A18, FINSEQ_1:58;

p2 | n2 = p2 by A19, FINSEQ_1:58;

then (p2 | n2) ^ (p1 /^ n2) = p2 ^ {} by A17, A18, FINSEQ_5:32, XXREAL_0:2

.= p2 by FINSEQ_1:34 ;

then A23: ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = {} by A20, FINSEQ_5:32;

p1 | n1 = p1 by A18, FINSEQ_1:58;

then (p1 | n1) ^ (p2 /^ n1) = p1 ^ {} by A20, FINSEQ_5:32

.= p1 by FINSEQ_1:34 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A17, A18, A21, A22, A23, FINSEQ_1:58, XXREAL_0:2; :: thesis: verum

suppose A24:
n1 < len p1
; :: thesis: crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

n1 <= len (p1 | n2)
then A25: ((p1 | n2) ^ (p2 /^ n2)) | n1 =
(p1 | n2) | n1
by FINSEQ_5:22

.= p1 | n1 by A17, FINSEQ_5:77 ;

A26: len (p1 | n1) = n1 by A24, FINSEQ_1:59;

then consider i being Nat such that

A27: (len (p1 | n1)) + i = n2 by A17, NAT_1:10;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

A28: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) ^ ((p2 /^ n1) | i) by A27, Th2;

len (p2 | n1) = n1 by A1, A3, A24, FINSEQ_1:59;

then (len (p2 | n1)) + i = n2 by A24, A27, FINSEQ_1:59;

then A29: crossover (p1,p2,n1,n2) = ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i) by A28, FINSEQ_5:36

.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i)) by FINSEQ_6:81

.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2) by A24, A27, FINSEQ_1:59 ;

A30: i = n2 - n1 by A26, A27;

n1 <= len (p2 | n2) then ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = ((p2 | n2) /^ n1) ^ (p1 /^ n2) by Th1

.= ((p2 /^ n1) | (n2 -' n1)) ^ (p1 /^ n2) by FINSEQ_5:80

.= ((p2 /^ n1) | i) ^ (p1 /^ n2) by A17, A30, XREAL_1:233 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A29, A25, FINSEQ_1:32; :: thesis: verum

end;.= p1 | n1 by A17, FINSEQ_5:77 ;

A26: len (p1 | n1) = n1 by A24, FINSEQ_1:59;

then consider i being Nat such that

A27: (len (p1 | n1)) + i = n2 by A17, NAT_1:10;

reconsider i = i as Element of NAT by ORDINAL1:def 12;

A28: ((p1 | n1) ^ (p2 /^ n1)) | n2 = (p1 | n1) ^ ((p2 /^ n1) | i) by A27, Th2;

len (p2 | n1) = n1 by A1, A3, A24, FINSEQ_1:59;

then (len (p2 | n1)) + i = n2 by A24, A27, FINSEQ_1:59;

then A29: crossover (p1,p2,n1,n2) = ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i) by A28, FINSEQ_5:36

.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i)) by FINSEQ_6:81

.= ((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2) by A24, A27, FINSEQ_1:59 ;

A30: i = n2 - n1 by A26, A27;

n1 <= len (p2 | n2) then ((p2 | n2) ^ (p1 /^ n2)) /^ n1 = ((p2 | n2) /^ n1) ^ (p1 /^ n2) by Th1

.= ((p2 /^ n1) | (n2 -' n1)) ^ (p1 /^ n2) by FINSEQ_5:80

.= ((p2 /^ n1) | i) ^ (p1 /^ n2) by A17, A30, XREAL_1:233 ;

hence crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1) by A29, A25, FINSEQ_1:32; :: thesis: verum