:: Basic Properties of Genetic Algorithm
:: by Akihiko Uchibori and Noboru Endou
::
:: Received April 24, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: GENEALG1:1
for D being non empty set
for f1, f2 being FinSequence of D
for n being Nat st n <= len f1 holds
(f1 ^ f2) /^ n = (f1 /^ n) ^ f2
proofend;

theorem Th2: :: GENEALG1:2
for D being non empty set
for f1, f2 being FinSequence of D
for i being Element of NAT holds (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)
proofend;

:: 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 GA-Space f ->  non empty ;
coherence
 not Union f is empty
proofend;
end;

definition
let S be Gene-Set;
mode Individual of S ->  FinSequence of GA-Space S means :Def1: :: GENEALG1:def 1
( len it = len S &amp; ( for i being Element of NAT st i in dom it holds
it . i in S . i ) );
existence
 ex b1 being FinSequence of GA-Space S st
( len b1 = len S &amp; ( for i being Element of NAT st i in dom b1 holds
b1 . i in S . i ) )
proofend;
end;

:: deftheorem Def1 defines Individual GENEALG1:def_1_:_
 for S being Gene-Set
for b2 being FinSequence of GA-Space S holds
( b2 is Individual of S iff ( len b2 = len S &amp; ( for i being Element of NAT st i in dom b2 holds
b2 . i in S . i ) ) );

begin

definition
let S be Gene-Set;
let p1, p2 be FinSequence of GA-Space S;
let n be Element of NAT ;
func crossover (p1,p2,n) ->  FinSequence of GA-Space S equals :: GENEALG1:def 2
(p1 | n) ^ (p2 /^ n);
correctness
coherence
(p1 | n) ^ (p2 /^ n) is FinSequence of GA-Space S;
;
end;

:: deftheorem  defines crossover GENEALG1:def_2_:_
 for S being Gene-Set
for p1, p2 being FinSequence of GA-Space S
for n being Element of NAT holds crossover (p1,p2,n) = (p1 | n) ^ (p2 /^ n);

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);

begin

theorem Th3: :: GENEALG1:3
for n being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n) is Individual of S
proofend;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n be Element of NAT ;
:: original:crossover
redefine func crossover (p1,p2,n) ->  Individual of S;
correctness
coherence
crossover (p1,p2,n) is Individual of S;
by Th3;
end;

theorem Th4: :: GENEALG1:4
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,0) = p2
proofend;

theorem Th5: :: GENEALG1:5
for n being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n >= len p1 holds
crossover (p1,p2,n) = p1
proofend;

begin

theorem Th6: :: GENEALG1:6
for n1, n2 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) is Individual of S
proofend;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2 be Element of NAT ;
:: original:crossover
redefine func crossover (p1,p2,n1,n2) ->  Individual of S;
correctness
coherence
crossover (p1,p2,n1,n2) is Individual of S;
by Th6;
end;

theorem Th7: :: GENEALG1:7
for n being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,0,n) = crossover (p2,p1,n)
proofend;

theorem Th8: :: GENEALG1:8
for n being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n,0) = crossover (p2,p1,n)
proofend;

theorem Th9: :: GENEALG1:9
for n1, n2 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) = crossover (p1,p2,n2)
proofend;

theorem Th10: :: GENEALG1:10
for n2, n1 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) = crossover (p1,p2,n1)
proofend;

theorem :: GENEALG1:11
for n1, n2 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n1 >= len p1 &amp; n2 >= len p1 holds
crossover (p1,p2,n1,n2) = p1
proofend;

theorem Th12: :: GENEALG1:12
for n1 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n1,n1) = p1
proofend;

theorem Th13: :: GENEALG1:13
for n1, n2 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)
proofend;

begin

theorem Th14: :: GENEALG1:14
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) is Individual of S
proofend;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3 be Element of NAT ;
:: original:crossover
redefine 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) &amp; crossover (p1,p2,n1,0,n3) = crossover (p2,p1,n1,n3) &amp; crossover (p1,p2,n1,n2,0) = crossover (p2,p1,n1,n2) )
proofend;

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) &amp; crossover (p1,p2,n1,0,0) = crossover (p1,p2,n1) &amp; crossover (p1,p2,0,n2,0) = crossover (p1,p2,n2) )
proofend;

theorem :: GENEALG1:17
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,0,0,0) = p2
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

theorem Th21: :: GENEALG1:21
for n1, n2, n3 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n1 >= len p1 &amp; n2 >= len p1 holds
crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n3)
proofend;

theorem :: GENEALG1:22
for n1, n3, n2 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n1 >= len p1 &amp; n3 >= len p1 holds
crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n2)
proofend;

theorem :: GENEALG1:23
for n2, n3, n1 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n2 >= len p1 &amp; n3 >= len p1 holds
crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n1)
proofend;

theorem :: GENEALG1:24
for n1, n2, n3 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n1 >= len p1 &amp; n2 >= len p1 &amp; n3 >= len p1 holds
crossover (p1,p2,n1,n2,n3) = p1
proofend;

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) &amp; crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n1,n3,n2) )
proofend;

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)
proofend;

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) &amp; crossover (p1,p2,n1,n2,n1) = crossover (p1,p2,n2) &amp; crossover (p1,p2,n1,n2,n2) = crossover (p1,p2,n1) )
proofend;

begin

theorem Th28: :: GENEALG1:28
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) is Individual of S
proofend;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3, n4 be Element of NAT ;
:: original:crossover
redefine 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) &amp; crossover (p1,p2,n1,0,n3,n4) = crossover (p2,p1,n1,n3,n4) &amp; crossover (p1,p2,n1,n2,0,n4) = crossover (p2,p1,n1,n2,n4) &amp; crossover (p1,p2,n1,n2,n3,0) = crossover (p2,p1,n1,n2,n3) )
proofend;

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) &amp; crossover (p1,p2,0,n2,0,n4) = crossover (p1,p2,n2,n4) &amp; crossover (p1,p2,0,n2,n3,0) = crossover (p1,p2,n2,n3) &amp; crossover (p1,p2,n1,0,n3,0) = crossover (p1,p2,n1,n3) &amp; crossover (p1,p2,n1,0,0,n4) = crossover (p1,p2,n1,n4) &amp; crossover (p1,p2,n1,n2,0,0) = crossover (p1,p2,n1,n2) )
proofend;

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) &amp; crossover (p1,p2,0,n2,0,0) = crossover (p2,p1,n2) &amp; crossover (p1,p2,0,0,n3,0) = crossover (p2,p1,n3) &amp; crossover (p1,p2,0,0,0,n4) = crossover (p2,p1,n4) )
proofend;

theorem Th32: :: GENEALG1:32
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,0,0,0,0) = p1
proofend;

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) ) &amp; ( n2 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n3,n4) ) &amp; ( n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n2,n4) ) &amp; ( n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n2,n3) ) )
proofend;

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 &amp; n2 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n4) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n4) ) &amp; ( n1 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n3) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n4) ) &amp; ( n2 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n3) ) &amp; ( n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n2) ) )
proofend;

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 &amp; n2 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4) ) &amp; ( n1 >= len p1 &amp; n2 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1) ) )
proofend;

theorem Th36: :: GENEALG1:36
for n1, n2, n3, n4 being Element of NAT
for S being Gene-Set
for p1, p2 being Individual of S st n1 >= len p1 &amp; n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 holds
crossover (p1,p2,n1,n2,n3,n4) = p1
proofend;

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) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n3,n2,n4) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n3,n4,n2) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n4,n3,n2) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n1,n3,n4) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n1,n4,n3) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n3,n1,n4) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n3,n4,n1) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n4,n1,n3) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n4,n3,n1) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n2,n1,n4) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n2,n4,n1) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n4,n1,n2) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n4,n2,n1) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n2,n3,n1) &amp; crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1) )
proofend;

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) &amp; crossover (p1,p2,n1,n2,n1,n4) = crossover (p1,p2,n2,n4) &amp; crossover (p1,p2,n1,n2,n3,n1) = crossover (p1,p2,n2,n3) &amp; crossover (p1,p2,n1,n2,n2,n4) = crossover (p1,p2,n1,n4) &amp; crossover (p1,p2,n1,n2,n3,n2) = crossover (p1,p2,n1,n3) &amp; crossover (p1,p2,n1,n2,n3,n3) = crossover (p1,p2,n1,n2) )
proofend;

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 &amp; crossover (p1,p2,n1,n2,n1,n2) = p1 &amp; crossover (p1,p2,n1,n2,n2,n1) = p1 )
proofend;

begin

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
proofend;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3, n4, n5 be Element of NAT ;
:: original:crossover
redefine 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) &amp; crossover (p1,p2,n1,0,n3,n4,n5) = crossover (p2,p1,n1,n3,n4,n5) &amp; crossover (p1,p2,n1,n2,0,n4,n5) = crossover (p2,p1,n1,n2,n4,n5) &amp; crossover (p1,p2,n1,n2,n3,0,n5) = crossover (p2,p1,n1,n2,n3,n5) &amp; crossover (p1,p2,n1,n2,n3,n4,0) = crossover (p2,p1,n1,n2,n3,n4) )
proofend;

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) &amp; crossover (p1,p2,0,n2,0,n4,n5) = crossover (p1,p2,n2,n4,n5) &amp; crossover (p1,p2,0,n2,n3,0,n5) = crossover (p1,p2,n2,n3,n5) &amp; crossover (p1,p2,0,n2,n3,n4,0) = crossover (p1,p2,n2,n3,n4) &amp; crossover (p1,p2,n1,0,0,n4,n5) = crossover (p1,p2,n1,n4,n5) &amp; crossover (p1,p2,n1,0,n3,0,n5) = crossover (p1,p2,n1,n3,n5) &amp; crossover (p1,p2,n1,0,n3,n4,0) = crossover (p1,p2,n1,n3,n4) &amp; crossover (p1,p2,n1,n2,0,0,n5) = crossover (p1,p2,n1,n2,n5) &amp; crossover (p1,p2,n1,n2,0,n4,0) = crossover (p1,p2,n1,n2,n4) &amp; crossover (p1,p2,n1,n2,n3,0,0) = crossover (p1,p2,n1,n2,n3) )
proofend;

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) &amp; crossover (p1,p2,0,0,n3,0,n5) = crossover (p2,p1,n3,n5) &amp; crossover (p1,p2,0,0,n3,n4,0) = crossover (p2,p1,n3,n4) &amp; crossover (p1,p2,0,n2,0,0,n5) = crossover (p2,p1,n2,n5) &amp; crossover (p1,p2,0,n2,0,n4,0) = crossover (p2,p1,n2,n4) &amp; crossover (p1,p2,0,n2,n3,0,0) = crossover (p2,p1,n2,n3) &amp; crossover (p1,p2,n1,0,0,0,n5) = crossover (p2,p1,n1,n5) &amp; crossover (p1,p2,n1,0,0,n4,0) = crossover (p2,p1,n1,n4) &amp; crossover (p1,p2,n1,0,n3,0,0) = crossover (p2,p1,n1,n3) &amp; crossover (p1,p2,n1,n2,0,0,0) = crossover (p2,p1,n1,n2) )
proofend;

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) &amp; crossover (p1,p2,0,0,0,n4,0) = crossover (p1,p2,n4) &amp; crossover (p1,p2,0,0,n3,0,0) = crossover (p1,p2,n3) &amp; crossover (p1,p2,0,n2,0,0,0) = crossover (p1,p2,n2) &amp; crossover (p1,p2,n1,0,0,0,0) = crossover (p1,p2,n1) )
proofend;

theorem :: GENEALG1:45
for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,0,0,0,0,0) = p2
proofend;

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) ) &amp; ( n2 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n3,n4,n5) ) &amp; ( n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n4,n5) ) &amp; ( n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n3,n5) ) &amp; ( n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n3,n4) ) )
proofend;

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 &amp; n2 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n4,n5) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n4,n5) ) &amp; ( n1 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n3,n5) ) &amp; ( n1 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n3,n4) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n4,n5) ) &amp; ( n2 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n3,n5) ) &amp; ( n2 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n3,n4) ) &amp; ( n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n5) ) &amp; ( n3 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n4) ) &amp; ( n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2,n3) ) )
proofend;

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 &amp; n2 >= len p1 &amp; n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n5) ) &amp; ( n1 >= len p1 &amp; n2 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n5) ) &amp; ( n1 >= len p1 &amp; n2 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n4) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n5) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n4) ) &amp; ( n1 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n3) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n5) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n4) ) &amp; ( n2 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n3) ) &amp; ( n3 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1,n2) ) )
proofend;

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 &amp; n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5) ) &amp; ( n1 >= len p1 &amp; n2 >= len p1 &amp; n3 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4) ) &amp; ( n1 >= len p1 &amp; n2 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3) ) &amp; ( n1 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2) ) &amp; ( n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n1) ) )
proofend;

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 &amp; n2 >= len p1 &amp; n3 >= len p1 &amp; n4 >= len p1 &amp; n5 >= len p1 holds
crossover (p1,p2,n1,n2,n3,n4,n5) = p1
proofend;

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) &amp; crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n2,n1,n4,n5) &amp; crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n2,n3,n1,n5) &amp; crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1) )
proofend;

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) &amp; crossover (p1,p2,n1,n2,n1,n4,n5) = crossover (p1,p2,n2,n4,n5) &amp; crossover (p1,p2,n1,n2,n3,n1,n5) = crossover (p1,p2,n2,n3,n5) &amp; crossover (p1,p2,n1,n2,n3,n4,n1) = crossover (p1,p2,n2,n3,n4) )
proofend;

begin

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
proofend;

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:crossover
redefine 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) &amp; crossover (p1,p2,n1,0,n3,n4,n5,n6) = crossover (p2,p1,n1,n3,n4,n5,n6) &amp; crossover (p1,p2,n1,n2,0,n4,n5,n6) = crossover (p2,p1,n1,n2,n4,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,0,n5,n6) = crossover (p2,p1,n1,n2,n3,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,0,n6) = crossover (p2,p1,n1,n2,n3,n4,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,0) = crossover (p2,p1,n1,n2,n3,n4,n5) )
proofend;

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) ) &amp; ( n2 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n1,n3,n4,n5,n6) ) &amp; ( n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n1,n2,n4,n5,n6) ) &amp; ( n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n1,n2,n3,n5,n6) ) &amp; ( n5 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n1,n2,n3,n4,n6) ) &amp; ( n6 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n1,n2,n3,n4,n5) ) )
proofend;

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) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n3,n2,n1,n4,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n4,n2,n3,n1,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n5,n2,n3,n4,n1,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,n6) = crossover (p1,p2,n6,n2,n3,n4,n5,n1) )
proofend;

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) &amp; crossover (p1,p2,n1,n2,n1,n4,n5,n6) = crossover (p1,p2,n2,n4,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,n1,n5,n6) = crossover (p1,p2,n2,n3,n5,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n1,n6) = crossover (p1,p2,n2,n3,n4,n6) &amp; crossover (p1,p2,n1,n2,n3,n4,n5,n1) = crossover (p1,p2,n2,n3,n4,n5) )
proofend;