:: Basic Properties of Genetic Algorithm :: by Akihiko Uchibori and Noboru Endou :: :: Received April 24, 1999 :: Copyright (c) 1999-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, FINSEQ_1, SUBSET_1, NUMBERS, NAT_1, XXREAL_0, ORDINAL4, RFINSEQ, ARYTM_3, ARYTM_1, FUNCT_1, RELAT_1, CARD_3, TARSKI, CARD_1, PARTFUN1, GENEALG1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, NAT_D, PARTFUN1, FINSEQ_1, CARD_3, RFINSEQ, XXREAL_0; constructors SETFAM_1, XXREAL_0, XREAL_0, NAT_1, CARD_3, RFINSEQ, PARTFUN1, BINARITH, REAL_1, NAT_D, RELSET_1; registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, XREAL_0, FINSEQ_1, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries reserve D for non empty set; reserve f1,f2 for FinSequence of D; reserve i,n,n1,n2,n3,n4,n5,n6 for Element of NAT; theorem :: GENEALG1:1 for n being Nat holds n <= len f1 implies (f1^f2)/^n = (f1/^n)^f2; theorem :: GENEALG1:2 (f1^f2)|(len f1 + i) = f1^(f2|i); :: Definitions of Gene-Set,GA-Space and Individual definition mode Gene-Set is non-empty non empty FinSequence; end; notation let S be Gene-Set; synonym GA-Space S for Union S; end; registration let f be non-empty non empty Function; cluster Union f -> non empty; end; definition let S be Gene-Set; mode Individual of S -> FinSequence of GA-Space S means :: GENEALG1:def 1 len it = len S & for i st i in dom it holds it.i in S.i; end; begin :: Definitions of several genetic operators definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n; func crossover(p1,p2,n) -> FinSequence of GA-Space S equals :: GENEALG1:def 2 (p1|n)^(p2/^n); end; definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n1,n2; func crossover(p1,p2,n1,n2) -> FinSequence of GA-Space S equals :: GENEALG1:def 3 crossover( crossover(p1,p2,n1),crossover(p2,p1,n1),n2); end; definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n1,n2,n3; func crossover(p1,p2,n1,n2,n3) -> FinSequence of GA-Space S equals :: GENEALG1:def 4 crossover (crossover(p1,p2,n1,n2),crossover(p2,p1,n1,n2),n3); end; definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n1,n2,n3,n4; func crossover(p1,p2,n1,n2,n3,n4) -> FinSequence of GA-Space S equals :: GENEALG1:def 5 crossover(crossover(p1,p2,n1,n2,n3),crossover(p2,p1,n1,n2,n3),n4); end; definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n1,n2,n3,n4,n5; func crossover(p1,p2,n1,n2,n3,n4,n5) -> FinSequence of GA-Space S equals :: GENEALG1:def 6 crossover(crossover(p1,p2,n1,n2,n3,n4),crossover(p2,p1,n1,n2,n3,n4),n5); end; definition let S be Gene-Set, p1,p2 be FinSequence of GA-Space S, n1,n2,n3,n4,n5,n6; func crossover(p1,p2,n1,n2,n3,n4,n5,n6) -> FinSequence of GA-Space S equals :: GENEALG1:def 7 crossover(crossover(p1,p2,n1,n2,n3,n4,n5), crossover(p2,p1,n1,n2,n3,n4,n5),n6); end; begin :: Properties of 1-point crossover reserve S for Gene-Set; reserve p1,p2 for Individual of S; theorem :: GENEALG1:3 crossover(p1,p2,n) is Individual of S; definition let S be Gene-Set, p1,p2 be Individual of S, n; redefine func crossover(p1,p2,n) -> Individual of S; end; theorem :: GENEALG1:4 crossover(p1,p2,0) = p2; theorem :: GENEALG1:5 n >= len p1 implies crossover(p1,p2,n) = p1; begin :: Properties of 2-points crossover theorem :: GENEALG1:6 crossover(p1,p2,n1,n2) is Individual of S; definition let S be Gene-Set, p1,p2 be Individual of S, n1,n2; redefine func crossover(p1,p2,n1,n2) -> Individual of S; end; theorem :: GENEALG1:7 crossover(p1,p2,0,n) = crossover(p2,p1,n); theorem :: GENEALG1:8 crossover(p1,p2,n,0) = crossover(p2,p1,n); theorem :: GENEALG1:9 n1 >= len p1 implies crossover(p1,p2,n1,n2)=crossover(p1,p2,n2); theorem :: GENEALG1:10 n2 >= len p1 implies crossover(p1,p2,n1,n2)=crossover(p1,p2,n1); theorem :: GENEALG1:11 n1 >= len p1 & n2 >= len p1 implies crossover(p1,p2,n1,n2)=p1; theorem :: GENEALG1:12 crossover(p1,p2,n1,n1) = p1; theorem :: GENEALG1:13 crossover(p1,p2,n1,n2) = crossover(p1,p2,n2,n1); begin :: Properties of 3-points crossover theorem :: GENEALG1:14 crossover(p1,p2,n1,n2,n3) is Individual of S; definition let S be Gene-Set, p1,p2 be Individual of S, n1,n2,n3; redefine func crossover(p1,p2,n1,n2,n3) -> Individual of S; end; theorem :: GENEALG1:15 crossover(p1,p2,0,n2,n3) = crossover(p2,p1,n2,n3) & crossover(p1 ,p2,n1,0,n3) = crossover(p2,p1,n1,n3) & crossover(p1,p2,n1,n2,0) = crossover(p2 ,p1,n1,n2); theorem :: GENEALG1:16 crossover(p1,p2,0,0,n3) = crossover(p1,p2,n3) & crossover(p1,p2,n1,0,0 ) = crossover(p1,p2,n1) & crossover(p1,p2,0,n2,0) = crossover(p1,p2,n2); theorem :: GENEALG1:17 crossover(p1,p2,0,0,0) = p2; theorem :: GENEALG1:18 n1 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2 ,n2,n3); theorem :: GENEALG1:19 n2 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2 ,n1,n3); theorem :: GENEALG1:20 n3 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2 ,n1,n2); theorem :: GENEALG1:21 n1 >= len p1 & n2 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n3); theorem :: GENEALG1:22 n1 >= len p1 & n3 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n2); theorem :: GENEALG1:23 n2 >= len p1 & n3 >= len p1 implies crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n1); theorem :: GENEALG1:24 n1 >= len p1 & n2 >= len p1 & n3 >= len p1 implies crossover(p1,p2,n1, n2,n3) = p1; theorem :: GENEALG1:25 crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n2,n1,n3) & crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n1,n3,n2); theorem :: GENEALG1:26 crossover(p1,p2,n1,n2,n3) = crossover(p1,p2,n3,n1,n2); theorem :: GENEALG1:27 crossover(p1,p2,n1,n1,n3)=crossover(p1,p2,n3) & crossover(p1,p2, n1,n2,n1)=crossover(p1,p2,n2) & crossover(p1,p2,n1,n2,n2)=crossover(p1,p2,n1) ; begin :: Properties of 4-points crossover theorem :: GENEALG1:28 crossover(p1,p2,n1,n2,n3,n4) is Individual of S; definition let S be Gene-Set, p1,p2 be Individual of S, n1,n2,n3,n4; redefine func crossover(p1,p2,n1,n2,n3,n4) -> Individual of S; end; theorem :: GENEALG1:29 crossover(p1,p2,0,n2,n3,n4) = crossover(p2,p1,n2,n3,n4) & crossover(p1,p2,n1,0,n3,n4) = crossover(p2,p1,n1,n3,n4) & crossover(p1,p2,n1,n2 ,0,n4) = crossover(p2,p1,n1,n2,n4) & crossover(p1,p2,n1,n2,n3,0) = crossover(p2 ,p1,n1,n2,n3); theorem :: GENEALG1:30 crossover(p1,p2,0,0,n3,n4) = crossover(p1,p2,n3,n4) & crossover( p1,p2,0,n2,0,n4) = crossover(p1,p2,n2,n4) & crossover(p1,p2,0,n2,n3,0) = crossover(p1,p2,n2,n3) & crossover(p1,p2,n1,0,n3,0) = crossover(p1,p2,n1,n3) & crossover(p1,p2,n1,0,0,n4) = crossover(p1,p2,n1,n4) & crossover(p1,p2,n1,n2,0,0 ) = crossover(p1,p2,n1,n2); theorem :: GENEALG1:31 crossover(p1,p2,n1,0,0,0) = crossover(p2,p1,n1) & crossover(p1, p2,0,n2,0,0) = crossover(p2,p1,n2) & crossover(p1,p2,0,0,n3,0) = crossover(p2, p1,n3) & crossover(p1,p2,0,0,0,n4) = crossover(p2,p1,n4); theorem :: GENEALG1:32 crossover(p1,p2,0,0,0,0) = p1; theorem :: GENEALG1:33 (n1 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover( p1,p2,n2,n3,n4)) & (n2 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n3,n4)) & (n3 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n2,n4)) & (n4 >= len p1 implies crossover(p1,p2,n1,n2,n3, n4) = crossover(p1,p2,n1,n2,n3)); theorem :: GENEALG1:34 (n1 >= len p1 & n2 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4 ) = crossover(p1,p2,n3,n4)) & (n1 >= len p1 & n3 >= len p1 implies crossover(p1 ,p2,n1,n2,n3,n4) = crossover(p1,p2,n2,n4)) & (n1 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n2,n3)) & (n2 >= len p1 & n3 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n4)) & (n2 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover( p1,p2,n1,n3)) & (n3 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3, n4) = crossover(p1,p2,n1,n2)); theorem :: GENEALG1:35 (n1 >= len p1 & n2 >= len p1 & n3 >= len p1 implies crossover(p1 ,p2,n1,n2,n3,n4) = crossover(p1,p2,n4)) & (n1 >= len p1 & n2 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n3)) & (n1 >= len p1 & n3 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n2)) & (n2 >= len p1 & n3 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1)); theorem :: GENEALG1:36 n1 >= len p1 & n2 >= len p1 & n3 >= len p1 & n4 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4) = p1; theorem :: GENEALG1:37 crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n2,n4,n3) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n3,n2,n4) & crossover(p1,p2, n1,n2,n3,n4) = crossover(p1,p2,n1,n3,n4,n2) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n1,n4,n3,n2) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2, n2,n1,n3,n4) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n2,n1,n4,n3) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n2,n3,n1,n4) & crossover(p1,p2, n1,n2,n3,n4) = crossover(p1,p2,n2,n3,n4,n1) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n2,n4,n1,n3) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2, n2,n4,n3,n1) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n3,n2,n1,n4) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n3,n2,n4,n1) & crossover(p1,p2, n1,n2,n3,n4) = crossover(p1,p2,n3,n4,n1,n2) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n3,n4,n2,n1) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2, n4,n2,n3,n1) & crossover(p1,p2,n1,n2,n3,n4) = crossover(p1,p2,n4,n3,n2,n1); theorem :: GENEALG1:38 crossover(p1,p2,n1,n1,n3,n4) = crossover(p1,p2,n3,n4) & crossover(p1,p2,n1,n2,n1,n4) = crossover(p1,p2,n2,n4) & crossover(p1,p2,n1,n2, n3,n1) = crossover(p1,p2,n2,n3) & crossover(p1,p2,n1,n2,n2,n4) = crossover(p1, p2,n1,n4) & crossover(p1,p2,n1,n2,n3,n2) = crossover(p1,p2,n1,n3) & crossover( p1,p2,n1,n2,n3,n3) = crossover(p1,p2,n1,n2); theorem :: GENEALG1:39 crossover(p1,p2,n1,n1,n3,n3) = p1 & crossover(p1,p2,n1,n2,n1,n2) = p1 & crossover(p1,p2,n1,n2,n2,n1) = p1; begin :: Properties of 5-points crossover theorem :: GENEALG1:40 crossover(p1,p2,n1,n2,n3,n4,n5) is Individual of S; definition let S be Gene-Set, p1,p2 be Individual of S, n1,n2,n3,n4,n5; redefine func crossover(p1,p2,n1,n2,n3,n4,n5) -> Individual of S; end; theorem :: GENEALG1:41 crossover(p1,p2,0,n2,n3,n4,n5)=crossover(p2,p1,n2,n3,n4,n5) & crossover(p1,p2,n1,0,n3,n4,n5) = crossover(p2,p1,n1,n3,n4,n5) & crossover(p1,p2 ,n1,n2,0,n4,n5) = crossover(p2,p1,n1,n2,n4,n5) & crossover(p1,p2,n1,n2,n3,0,n5) = crossover(p2,p1,n1,n2,n3,n5) & crossover(p1,p2,n1,n2,n3,n4,0) = crossover(p2, p1,n1,n2,n3,n4); theorem :: GENEALG1:42 crossover(p1,p2,0,0,n3,n4,n5)=crossover(p1,p2,n3,n4,n5) & crossover(p1 ,p2,0,n2,0,n4,n5)=crossover(p1,p2,n2,n4,n5) & crossover(p1,p2,0,n2,n3,0,n5)= crossover(p1,p2,n2,n3,n5) & crossover(p1,p2,0,n2,n3,n4,0)=crossover(p1,p2,n2,n3 ,n4) & crossover(p1,p2,n1,0,0,n4,n5)=crossover(p1,p2,n1,n4,n5) & crossover(p1, p2,n1,0,n3,0,n5)=crossover(p1,p2,n1,n3,n5) & crossover(p1,p2,n1,0,n3,n4,0)= crossover(p1,p2,n1,n3,n4) & crossover(p1,p2,n1,n2,0,0,n5)=crossover(p1,p2,n1,n2 ,n5) & crossover(p1,p2,n1,n2,0,n4,0)=crossover(p1,p2,n1,n2,n4) & crossover(p1, p2,n1,n2,n3,0,0)=crossover(p1,p2,n1,n2,n3); theorem :: GENEALG1:43 crossover(p1,p2,0,0,0,n4,n5)=crossover(p2,p1,n4,n5) & crossover(p1,p2, 0,0,n3,0,n5)=crossover(p2,p1,n3,n5) & crossover(p1,p2,0,0,n3,n4,0)=crossover(p2 ,p1,n3,n4) & crossover(p1,p2,0,n2,0,0,n5)=crossover(p2,p1,n2,n5) & crossover(p1 ,p2,0,n2,0,n4,0)=crossover(p2,p1,n2,n4) & crossover(p1,p2,0,n2,n3,0,0)= crossover(p2,p1,n2,n3) & crossover(p1,p2,n1,0,0,0,n5)=crossover(p2,p1,n1,n5) & crossover(p1,p2,n1,0,0,n4,0)=crossover(p2,p1,n1,n4) & crossover(p1,p2,n1,0,n3,0 ,0)=crossover(p2,p1,n1,n3) & crossover(p1,p2,n1,n2,0,0,0)=crossover(p2,p1,n1,n2 ); theorem :: GENEALG1:44 crossover(p1,p2,0,0,0,0,n5)=crossover(p1,p2,n5) & crossover(p1,p2,0,0, 0,n4,0)=crossover(p1,p2,n4) & crossover(p1,p2,0,0,n3,0,0)=crossover(p1,p2,n3) & crossover(p1,p2,0,n2,0,0,0)=crossover(p1,p2,n2) & crossover(p1,p2,n1,0,0,0,0)= crossover(p1,p2,n1); theorem :: GENEALG1:45 crossover(p1,p2,0,0,0,0,0)=p2; theorem :: GENEALG1:46 (n1>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1 ,p2,n2,n3,n4,n5)) & (n2>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)= crossover(p1,p2,n1,n3,n4,n5)) & (n3>=len p1 implies crossover(p1,p2,n1,n2,n3,n4 ,n5)=crossover(p1,p2,n1,n2,n4,n5)) & (n4>=len p1 implies crossover(p1,p2,n1,n2, n3,n4,n5)=crossover(p1,p2,n1,n2,n3,n5)) & (n5>=len p1 implies crossover(p1,p2, n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n2,n3,n4)); theorem :: GENEALG1:47 (n1>=len p1 & n2>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)= crossover(p1,p2,n3,n4,n5)) & (n1>=len p1 & n3>=len p1 implies crossover(p1,p2, n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n4,n5)) & (n1>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n3,n5)) & (n1>=len p1 & n5>= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n3,n4)) & (n2 >=len p1 & n3>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2, n1,n4,n5)) & (n2>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)= crossover(p1,p2,n1,n3,n5)) & (n2>=len p1 & n5>=len p1 implies crossover(p1,p2, n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n3,n4)) & (n3>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n2,n5)) & (n3>=len p1 & n5>= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n2,n4)) & (n4 >=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2, n1,n2,n3)); theorem :: GENEALG1:48 (n1>=len p1 & n2>=len p1 & n3>=len p1 implies crossover(p1,p2,n1,n2,n3 ,n4,n5)=crossover(p1,p2,n4,n5)) & (n1>=len p1 & n2>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n3,n5)) & (n1>=len p1 & n2>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n3,n4)) & (n1>=len p1 & n3>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5) =crossover(p1,p2,n2,n5)) & (n1>=len p1 & n3>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n4)) & (n1>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n3)) & (n2>=len p1 & n3>=len p1 & n4>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5) =crossover(p1,p2,n1,n5)) & (n2>=len p1 & n3>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n4)) & (n2>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n1,n3)) & (n3>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5) =crossover(p1,p2,n1,n2)); theorem :: GENEALG1:49 (n1>=len p1 & n2>=len p1 & n3>=len p1 & n4>=len p1 implies crossover( p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n5)) & (n1>=len p1 & n2>=len p1 & n3>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n4)) & (n1>=len p1 & n2>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1, n2,n3,n4,n5)=crossover(p1,p2,n3)) & (n1>=len p1 & n3>=len p1 & n4>=len p1 & n5 >=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2)) & (n2>= len p1 & n3>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3, n4,n5)=crossover(p1,p2,n1)); theorem :: GENEALG1:50 n1>=len p1 & n2>=len p1 & n3>=len p1 & n4>=len p1 & n5>=len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5)=p1; theorem :: GENEALG1:51 crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n2,n1,n3,n4,n5) & crossover(p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n3,n2,n1,n4,n5) & crossover( p1,p2,n1,n2,n3,n4,n5)=crossover(p1,p2,n4,n2,n3,n1,n5) & crossover(p1,p2,n1,n2, n3,n4,n5)=crossover(p1,p2,n5,n2,n3,n4,n1); theorem :: GENEALG1:52 crossover(p1,p2,n1,n1,n3,n4,n5)=crossover(p1,p2,n3,n4,n5) & crossover(p1,p2,n1,n2,n1,n4,n5)=crossover(p1,p2,n2,n4,n5) & crossover(p1,p2,n1, n2,n3,n1,n5)=crossover(p1,p2,n2,n3,n5) & crossover(p1,p2,n1,n2,n3,n4,n1)= crossover(p1,p2,n2,n3,n4); begin :: Properties of 6-points crossover theorem :: GENEALG1:53 crossover(p1,p2,n1,n2,n3,n4,n5,n6) is Individual of S; definition let S be Gene-Set,p1,p2 be Individual of S,n1,n2,n3,n4,n5,n6; redefine func crossover(p1,p2,n1,n2,n3,n4,n5,n6) -> Individual of S; end; theorem :: GENEALG1:54 crossover(p1,p2,0,n2,n3,n4,n5,n6)=crossover(p2,p1,n2,n3,n4,n5,n6) & crossover(p1,p2,n1,0,n3,n4,n5,n6)=crossover(p2,p1,n1,n3,n4,n5,n6) & crossover( p1,p2,n1,n2,0,n4,n5,n6)=crossover(p2,p1,n1,n2,n4,n5,n6) & crossover(p1,p2,n1,n2 ,n3,0,n5,n6)=crossover(p2,p1,n1,n2,n3,n5,n6) & crossover(p1,p2,n1,n2,n3,n4,0,n6 )=crossover(p2,p1,n1,n2,n3,n4,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,0)=crossover (p2,p1,n1,n2,n3,n4,n5); theorem :: GENEALG1:55 (n1 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1, p2,n2,n3,n4,n5,n6)) & (n2 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5,n6)= crossover(p1,p2,n1,n3,n4,n5,n6)) & (n3 >= len p1 implies crossover(p1,p2,n1,n2, n3,n4,n5,n6)=crossover(p1,p2,n1,n2,n4,n5,n6)) & (n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n1,n2,n3,n5,n6)) & (n5 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n1,n2,n3,n4,n6)) & ( n6 >= len p1 implies crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n1,n2, n3,n4,n5)); theorem :: GENEALG1:56 crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n2,n1,n3,n4, n5,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n3,n2,n1,n4,n5,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n4,n2,n3,n1,n5,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n5,n2,n3,n4,n1,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,n6)=crossover(p1,p2,n6,n2,n3,n4,n5,n1); theorem :: GENEALG1:57 crossover(p1,p2,n1,n1,n3,n4,n5,n6)=crossover(p1,p2,n3,n4,n5,n6) & crossover(p1,p2,n1,n2,n1,n4,n5,n6)=crossover(p1,p2,n2,n4,n5,n6) & crossover(p1, p2,n1,n2,n3,n1,n5,n6)=crossover(p1,p2,n2,n3,n5,n6) & crossover(p1,p2,n1,n2,n3, n4,n1,n6)=crossover(p1,p2,n2,n3,n4,n6) & crossover(p1,p2,n1,n2,n3,n4,n5,n1)= crossover(p1,p2,n2,n3,n4,n5);