:: by Akihiko Uchibori and Noboru Endou

::

:: Received April 24, 1999

:: Copyright (c) 1999-2019 Association of Mizar Users

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

for f1, f2 being FinSequence of D

for n being Nat st n <= len f1 holds

(f1 ^ f2) /^ n = (f1 /^ n) ^ f2

proof end;

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)

for f1, f2 being FinSequence of D

for i being Element of NAT holds (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)

proof end;

:: Definitions of Gene-Set,GA-Space and Individual

definition

let S be Gene-Set;

ex b_{1} being FinSequence of GA-Space S st

( len b_{1} = len S & ( for i being Element of NAT st i in dom b_{1} holds

b_{1} . i in S . i ) )

end;
mode Individual of S -> FinSequence of GA-Space S means :Def1: :: GENEALG1:def 1

( len it = len S & ( for i being Element of NAT st i in dom it holds

it . i in S . i ) );

existence ( len it = len S & ( for i being Element of NAT st i in dom it holds

it . i in S . i ) );

ex b

( len b

b

proof end;

:: deftheorem Def1 defines Individual GENEALG1:def 1 :

for S being Gene-Set

for b_{2} being FinSequence of GA-Space S holds

( b_{2} is Individual of S iff ( len b_{2} = len S & ( for i being Element of NAT st i in dom b_{2} holds

b_{2} . i in S . i ) ) );

for S being Gene-Set

for b

( b

b

definition

let S be Gene-Set;

let p1, p2 be FinSequence of GA-Space S;

let n be Element of NAT ;

correctness

coherence

(p1 | n) ^ (p2 /^ n) is FinSequence of GA-Space S;

;

end;
let p1, p2 be FinSequence of GA-Space S;

let n be Element of NAT ;

correctness

coherence

(p1 | n) ^ (p2 /^ n) is FinSequence of GA-Space S;

;

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

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 ;

coherence

crossover ((crossover (p1,p2,n1)),(crossover (p2,p1,n1)),n2) is FinSequence of GA-Space S;

;

end;
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 crossover ((crossover (p1,p2,n1)),(crossover (p2,p1,n1)),n2);

coherence

crossover ((crossover (p1,p2,n1)),(crossover (p2,p1,n1)),n2) is FinSequence of GA-Space S;

;

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

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 ;

coherence

crossover ((crossover (p1,p2,n1,n2)),(crossover (p2,p1,n1,n2)),n3) is FinSequence of GA-Space S;

;

end;
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 crossover ((crossover (p1,p2,n1,n2)),(crossover (p2,p1,n1,n2)),n3);

coherence

crossover ((crossover (p1,p2,n1,n2)),(crossover (p2,p1,n1,n2)),n3) is FinSequence of GA-Space S;

;

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

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 ;

coherence

crossover ((crossover (p1,p2,n1,n2,n3)),(crossover (p2,p1,n1,n2,n3)),n4) is FinSequence of GA-Space S;

;

end;
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 crossover ((crossover (p1,p2,n1,n2,n3)),(crossover (p2,p1,n1,n2,n3)),n4);

coherence

crossover ((crossover (p1,p2,n1,n2,n3)),(crossover (p2,p1,n1,n2,n3)),n4) is FinSequence of GA-Space S;

;

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

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 ;

coherence

crossover ((crossover (p1,p2,n1,n2,n3,n4)),(crossover (p2,p1,n1,n2,n3,n4)),n5) is FinSequence of GA-Space S;

;

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

coherence

crossover ((crossover (p1,p2,n1,n2,n3,n4)),(crossover (p2,p1,n1,n2,n3,n4)),n5) is FinSequence of GA-Space S;

;

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

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 ;

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

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;

;

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

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

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

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n) is Individual of S

proof end;

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

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

for S being Gene-Set

for p1, p2 being Individual of S st n >= len p1 holds

crossover (p1,p2,n) = p1

proof end;

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

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) is Individual of S

proof end;

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

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)

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,0,n) = crossover (p2,p1,n)

proof end;

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)

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n,0) = crossover (p2,p1,n)

proof end;

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)

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)

proof end;

theorem Th10: :: GENEALG1:10

for n1, n2 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)

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)

proof end;

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 & n2 >= len p1 holds

crossover (p1,p2,n1,n2) = p1

for S being Gene-Set

for p1, p2 being Individual of S st n1 >= len p1 & n2 >= len p1 holds

crossover (p1,p2,n1,n2) = p1

proof end;

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

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n1) = p1

proof end;

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)

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) = crossover (p1,p2,n2,n1)

proof end;

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

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2,n3) is Individual of S

proof end;

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

theorem Th15: :: GENEALG1:15

for n1, n2, n3 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) )

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

proof end;

theorem :: GENEALG1:16

for n1, n2, n3 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) )

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

proof end;

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)

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)

proof end;

theorem Th19: :: GENEALG1:19

for n1, n2, 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)

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)

proof end;

theorem Th20: :: GENEALG1:20

for n1, n2, n3 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)

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)

proof end;

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 & n2 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n3)

for S being Gene-Set

for p1, p2 being Individual of S st n1 >= len p1 & n2 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n3)

proof end;

theorem :: GENEALG1:22

for n1, n2, n3 being Element of NAT

for S being Gene-Set

for p1, p2 being Individual of S st n1 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n2)

for S being Gene-Set

for p1, p2 being Individual of S st n1 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n2)

proof end;

theorem :: GENEALG1:23

for n1, n2, n3 being Element of NAT

for S being Gene-Set

for p1, p2 being Individual of S st n2 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n1)

for S being Gene-Set

for p1, p2 being Individual of S st n2 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = crossover (p1,p2,n1)

proof end;

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 & n2 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = p1

for S being Gene-Set

for p1, p2 being Individual of S st n1 >= len p1 & n2 >= len p1 & n3 >= len p1 holds

crossover (p1,p2,n1,n2,n3) = p1

proof end;

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

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

proof end;

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)

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)

proof end;

theorem Th27: :: GENEALG1:27

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

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

proof end;

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

for S being Gene-Set

for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2,n3,n4) is Individual of S

proof end;

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

theorem Th29: :: GENEALG1:29

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

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

proof end;

theorem Th30: :: GENEALG1:30

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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 & n2 >= len p1 & n3 >= len p1 & n4 >= len p1 holds

crossover (p1,p2,n1,n2,n3,n4) = p1

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 holds

crossover (p1,p2,n1,n2,n3,n4) = p1

proof end;

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

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

proof end;

theorem Th38: :: GENEALG1:38

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

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

proof end;

theorem :: GENEALG1:39

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

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 )

proof end;

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

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

proof end;

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

theorem Th41: :: GENEALG1:41

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

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

proof end;

theorem :: GENEALG1:42

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

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

proof end;

theorem :: GENEALG1:43

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

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

proof end;

theorem :: GENEALG1:44

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

theorem Th52: :: GENEALG1:52

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

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

proof end;

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

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

proof end;

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

theorem :: GENEALG1:54

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

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

proof end;

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

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

proof end;

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

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

proof end;

theorem :: GENEALG1:57

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

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

proof end;