begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines Individual GENEALG1:def 1 :
begin
:: 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
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
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
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
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
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;
begin
theorem Th3:
theorem Th4:
theorem Th5:
begin
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
begin
theorem Th14:
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3 be
Element of
NAT ;
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:
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
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
theorem Th18:
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:
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:
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:
theorem
theorem
theorem
theorem Th25:
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:
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:
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 )
begin
theorem Th28:
definition
let S be
Gene-Set;
let p1,
p2 be
Individual of
S;
let n1,
n2,
n3,
n4 be
Element of
NAT ;
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:
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:
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:
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:
theorem Th33:
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:
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:
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:
theorem Th37:
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:
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
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 )
begin
theorem Th40:
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 ;
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:
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
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
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
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
theorem Th46:
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
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
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
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
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:
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:
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 )
begin
theorem Th53:
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 ;
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
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
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:
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
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 )