:: Basic Properties of Genetic Algorithm
::  by Akihiko Uchibori and Noboru Endou
::
:: Received April 24, 1999
:: Copyright (c) 1999-2021 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);