:: Basic Properties of Genetic Algorithm
:: by Akihiko Uchibori and Noboru Endou
::
:: Received April 24, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: GENEALG1:1
theorem Th2: :: GENEALG1:2
:: deftheorem Def1 defines Individual GENEALG1:def 1 :
:: deftheorem defines crossover GENEALG1:def 2 :
definition
let S be
Gene-Set;
let p1,
p2 be
FinSequence of
GA-Space S;
let n1,
n2 be
Element of
NAT ;
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;
correctness
coherence
crossover (crossover p1,p2,n1),(crossover p2,p1,n1),n2 is FinSequence of GA-Space S;
;
end;
:: deftheorem defines crossover GENEALG1:def 3 :
for
S being
Gene-Set for
p1,
p2 being
FinSequence of
GA-Space S for
n1,
n2 being
Element of
NAT holds
crossover p1,
p2,
n1,
n2 = crossover (crossover p1,p2,n1),
(crossover p2,p1,n1),
n2;
definition
let S be
Gene-Set;
let p1,
p2 be
FinSequence of
GA-Space S;
let n1,
n2,
n3 be
Element of
NAT ;
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;
correctness
coherence
crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2),n3 is FinSequence of GA-Space S;
;
end;
:: deftheorem defines crossover GENEALG1:def 4 :
for
S being
Gene-Set for
p1,
p2 being
FinSequence of
GA-Space S for
n1,
n2,
n3 being
Element of
NAT holds
crossover p1,
p2,
n1,
n2,
n3 = crossover (crossover p1,p2,n1,n2),
(crossover p2,p1,n1,n2),
n3;
definition
let S be
Gene-Set;
let p1,
p2 be
FinSequence of
GA-Space S;
let n1,
n2,
n3,
n4 be
Element of
NAT ;
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;
correctness
coherence
crossover (crossover p1,p2,n1,n2,n3),(crossover p2,p1,n1,n2,n3),n4 is FinSequence of GA-Space S;
;
end;
:: deftheorem defines crossover GENEALG1:def 5 :
for
S being
Gene-Set for
p1,
p2 being
FinSequence of
GA-Space S for
n1,
n2,
n3,
n4 being
Element of
NAT holds
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover (crossover p1,p2,n1,n2,n3),
(crossover p2,p1,n1,n2,n3),
n4;
definition
let S be
Gene-Set;
let p1,
p2 be
FinSequence of
GA-Space S;
let n1,
n2,
n3,
n4,
n5 be
Element of
NAT ;
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;
correctness
coherence
crossover (crossover p1,p2,n1,n2,n3,n4),(crossover p2,p1,n1,n2,n3,n4),n5 is FinSequence of GA-Space S;
;
end;
:: deftheorem defines crossover GENEALG1:def 6 :
for
S being
Gene-Set for
p1,
p2 being
FinSequence of
GA-Space S for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT holds
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 = crossover (crossover p1,p2,n1,n2,n3,n4),
(crossover p2,p1,n1,n2,n3,n4),
n5;
definition
let S be
Gene-Set;
let p1,
p2 be
FinSequence of
GA-Space S;
let n1,
n2,
n3,
n4,
n5,
n6 be
Element of
NAT ;
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;
correctness
coherence
crossover (crossover p1,p2,n1,n2,n3,n4,n5),(crossover p2,p1,n1,n2,n3,n4,n5),n6 is FinSequence of GA-Space S;
;
end;
:: deftheorem defines crossover GENEALG1:def 7 :
for
S being
Gene-Set for
p1,
p2 being
FinSequence of
GA-Space S for
n1,
n2,
n3,
n4,
n5,
n6 being
Element of
NAT holds
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5,
n6 = crossover (crossover p1,p2,n1,n2,n3,n4,n5),
(crossover p2,p1,n1,n2,n3,n4,n5),
n6;
theorem Th3: :: GENEALG1:3
theorem Th4: :: GENEALG1:4
theorem Th5: :: GENEALG1:5
theorem Th6: :: GENEALG1:6
theorem Th7: :: GENEALG1:7
theorem Th8: :: GENEALG1:8
theorem Th9: :: GENEALG1:9
theorem Th10: :: GENEALG1:10
theorem :: GENEALG1:11
theorem Th12: :: GENEALG1:12
theorem Th13: :: GENEALG1:13
theorem Th14: :: GENEALG1:14
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3 be
Element of
NAT ;
:: original: crossoverredefine func crossover p1,
p2,
n1,
n2,
n3 -> Individual of
S;
correctness
coherence
crossover p1,p2,n1,n2,n3 is Individual of S;
by Th14;
end;
theorem Th15: :: GENEALG1:15
for
n2,
n3,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n3,
n1,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
theorem Th18: :: GENEALG1:18
for
n1,
n2,
n3 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S st
n1 >= len p1 holds
crossover p1,
p2,
n1,
n2,
n3 = crossover p1,
p2,
n2,
n3
theorem Th19: :: GENEALG1:19
for
n2,
n1,
n3 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S st
n2 >= len p1 holds
crossover p1,
p2,
n1,
n2,
n3 = crossover p1,
p2,
n1,
n3
theorem Th20: :: GENEALG1:20
for
n3,
n1,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S st
n3 >= len p1 holds
crossover p1,
p2,
n1,
n2,
n3 = crossover p1,
p2,
n1,
n2
theorem Th21: :: GENEALG1:21
theorem :: GENEALG1:22
theorem :: GENEALG1:23
theorem :: GENEALG1:24
theorem Th25: :: GENEALG1:25
for
n1,
n2,
n3 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th26: :: GENEALG1:26
for
n1,
n2,
n3 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
crossover p1,
p2,
n1,
n2,
n3 = crossover p1,
p2,
n3,
n1,
n2
theorem Th27: :: GENEALG1:27
for
n1,
n3,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 )
theorem Th28: :: GENEALG1:28
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3,
n4 be
Element of
NAT ;
:: original: crossoverredefine func crossover p1,
p2,
n1,
n2,
n3,
n4 -> Individual of
S;
correctness
coherence
crossover p1,p2,n1,n2,n3,n4 is Individual of S;
by Th28;
end;
theorem Th29: :: GENEALG1:29
for
n2,
n3,
n4,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th30: :: GENEALG1:30
for
n3,
n4,
n2,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th31: :: GENEALG1:31
for
n1,
n2,
n3,
n4 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th32: :: GENEALG1:32
theorem Th33: :: GENEALG1:33
for
n1,
n2,
n3,
n4 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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 Th34: :: GENEALG1:34
for
n1,
n2,
n3,
n4 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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 Th35: :: GENEALG1:35
for
n1,
n2,
n3,
n4 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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 Th36: :: GENEALG1:36
theorem Th37: :: GENEALG1:37
for
n1,
n2,
n3,
n4 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th38: :: GENEALG1:38
for
n1,
n3,
n4,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n1,
n3,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
crossover p1,
p2,
n1,
n1,
n3,
n3 = p1 &
crossover p1,
p2,
n1,
n2,
n1,
n2 = p1 &
crossover p1,
p2,
n1,
n2,
n2,
n1 = p1 )
theorem Th40: :: GENEALG1:40
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 is
Individual of
S
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3,
n4,
n5 be
Element of
NAT ;
:: original: crossoverredefine func crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 -> Individual of
S;
correctness
coherence
crossover p1,p2,n1,n2,n3,n4,n5 is Individual of S;
by Th40;
end;
theorem Th41: :: GENEALG1:41
for
n2,
n3,
n4,
n5,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n3,
n4,
n5,
n2,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n4,
n5,
n3,
n2,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n5,
n4,
n3,
n2,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
theorem Th46: :: GENEALG1:46
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S st
n1 >= len p1 &
n2 >= len p1 &
n3 >= len p1 &
n4 >= len p1 &
n5 >= len p1 holds
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 = p1
theorem Th51: :: GENEALG1:51
for
n1,
n2,
n3,
n4,
n5 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 Th52: :: GENEALG1:52
for
n1,
n3,
n4,
n5,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 )
theorem Th53: :: GENEALG1:53
for
n1,
n2,
n3,
n4,
n5,
n6 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5,
n6 is
Individual of
S
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3,
n4,
n5,
n6 be
Element of
NAT ;
:: original: crossoverredefine func crossover p1,
p2,
n1,
n2,
n3,
n4,
n5,
n6 -> Individual of
S;
correctness
coherence
crossover p1,p2,n1,n2,n3,n4,n5,n6 is Individual of S;
by Th53;
end;
theorem :: GENEALG1:54
for
n2,
n3,
n4,
n5,
n6,
n1 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n1,
n2,
n3,
n4,
n5,
n6 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
( (
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 Th56: :: GENEALG1:56
for
n1,
n2,
n3,
n4,
n5,
n6 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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
for
n1,
n3,
n4,
n5,
n6,
n2 being
Element of
NAT for
S being
Gene-Set for
p1,
p2 being
Individual of
S holds
(
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 )