:: GENEALG1 semantic presentation

theorem Th1: :: GENEALG1:1
for b1 being non empty set
for b2, b3 being FinSequence of b1
for b4 being Nat st b4 <= len b2 holds
(b2 ^ b3) /^ b4 = (b2 /^ b4) ^ b3
proof end;

theorem Th2: :: GENEALG1:2
for b1 being non empty set
for b2, b3 being FinSequence of b1
for b4 being Nat holds (b2 ^ b3) | ((len b2) + b4) = b2 ^ (b3 | b4)
proof end;

definition
mode Gene-Set is non empty non-empty FinSequence;
end;

notation
let c1 be Gene-Set;
synonym GA-Space c1 for Union c1;
end;

registration
let c1 be non empty non-empty Function;
cluster GA-Space a1 -> non empty ;
coherence
not Union c1 is empty
proof end;
end;

definition
let c1 be Gene-Set;
mode Individual of c1 -> FinSequence of GA-Space a1 means :Def1: :: GENEALG1:def 1
( len a2 = len a1 & ( for b1 being Nat st b1 in dom a2 holds
a2 . b1 in a1 . b1 ) );
existence
ex b1 being FinSequence of GA-Space c1 st
( len b1 = len c1 & ( for b2 being Nat st b2 in dom b1 holds
b1 . b2 in c1 . b2 ) )
proof end;
end;

:: deftheorem Def1 defines Individual GENEALG1:def 1 :
for b1 being Gene-Set
for b2 being FinSequence of GA-Space b1 holds
( b2 is Individual of b1 iff ( len b2 = len b1 & ( for b3 being Nat st b3 in dom b2 holds
b2 . b3 in b1 . b3 ) ) );

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4 be Nat;
func crossover c2,c3,c4 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 2
(a2 | a4) ^ (a3 /^ a4);
correctness
coherence
(c2 | c4) ^ (c3 /^ c4) is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def2 defines crossover GENEALG1:def 2 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4 being Nat holds crossover b2,b3,b4 = (b2 | b4) ^ (b3 /^ b4);

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4, c5 be Nat;
func crossover c2,c3,c4,c5 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 3
 crossover (crossover a2,a3,a4),(crossover a3,a2,a4),a5;
correctness
coherence
crossover (crossover c2,c3,c4),(crossover c3,c2,c4),c5 is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def3 defines crossover GENEALG1:def 3 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4, b5 being Nat holds crossover b2,b3,b4,b5 = crossover (crossover b2,b3,b4),(crossover b3,b2,b4),b5;

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4, c5, c6 be Nat;
func crossover c2,c3,c4,c5,c6 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 4
 crossover (crossover a2,a3,a4,a5),(crossover a3,a2,a4,a5),a6;
correctness
coherence
crossover (crossover c2,c3,c4,c5),(crossover c3,c2,c4,c5),c6 is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def4 defines crossover GENEALG1:def 4 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4, b5, b6 being Nat holds crossover b2,b3,b4,b5,b6 = crossover (crossover b2,b3,b4,b5),(crossover b3,b2,b4,b5),b6;

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4, c5, c6, c7 be Nat;
func crossover c2,c3,c4,c5,c6,c7 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 5
 crossover (crossover a2,a3,a4,a5,a6),(crossover a3,a2,a4,a5,a6),a7;
correctness
coherence
crossover (crossover c2,c3,c4,c5,c6),(crossover c3,c2,c4,c5,c6),c7 is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def5 defines crossover GENEALG1:def 5 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4, b5, b6, b7 being Nat holds crossover b2,b3,b4,b5,b6,b7 = crossover (crossover b2,b3,b4,b5,b6),(crossover b3,b2,b4,b5,b6),b7;

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4, c5, c6, c7, c8 be Nat;
func crossover c2,c3,c4,c5,c6,c7,c8 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 6
 crossover (crossover a2,a3,a4,a5,a6,a7),(crossover a3,a2,a4,a5,a6,a7),a8;
correctness
coherence
crossover (crossover c2,c3,c4,c5,c6,c7),(crossover c3,c2,c4,c5,c6,c7),c8 is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def6 defines crossover GENEALG1:def 6 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4, b5, b6, b7, b8 being Nat holds crossover b2,b3,b4,b5,b6,b7,b8 = crossover (crossover b2,b3,b4,b5,b6,b7),(crossover b3,b2,b4,b5,b6,b7),b8;

definition
let c1 be Gene-Set;
let c2, c3 be FinSequence of GA-Space c1;
let c4, c5, c6, c7, c8, c9 be Nat;
func crossover c2,c3,c4,c5,c6,c7,c8,c9 -> FinSequence of GA-Space a1 equals :: GENEALG1:def 7
 crossover (crossover a2,a3,a4,a5,a6,a7,a8),(crossover a3,a2,a4,a5,a6,a7,a8),a9;
correctness
coherence
crossover (crossover c2,c3,c4,c5,c6,c7,c8),(crossover c3,c2,c4,c5,c6,c7,c8),c9 is FinSequence of GA-Space c1;
;
end;

:: deftheorem Def7 defines crossover GENEALG1:def 7 :
for b1 being Gene-Set
for b2, b3 being FinSequence of GA-Space b1
for b4, b5, b6, b7, b8, b9 being Nat holds crossover b2,b3,b4,b5,b6,b7,b8,b9 = crossover (crossover b2,b3,b4,b5,b6,b7,b8),(crossover b3,b2,b4,b5,b6,b7,b8),b9;

theorem Th3: :: GENEALG1:3
for b1 being Nat
for b2 being Gene-Set
for b3, b4 being Individual of b2 holds crossover b3,b4,b1 is Individual of b2
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4 be Nat;
redefine func crossover as crossover c2,c3,c4 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4 is Individual of c1;
by Th3;
end;

theorem Th4: :: GENEALG1:4
for b1 being Gene-Set
for b2, b3 being Individual of b1 holds crossover b2,b3,0 = b3
proof end;

theorem Th5: :: GENEALG1:5
for b1 being Nat
for b2 being Gene-Set
for b3, b4 being Individual of b2 st b1 >= len b3 holds
crossover b3,b4,b1 = b3
proof end;

theorem Th6: :: GENEALG1:6
for b1, b2 being Nat
for b3 being Gene-Set
for b4, b5 being Individual of b3 holds crossover b4,b5,b1,b2 is Individual of b3
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4, c5 be Nat;
redefine func crossover as crossover c2,c3,c4,c5 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4,c5 is Individual of c1;
by Th6;
end;

theorem Th7: :: GENEALG1:7
for b1 being Nat
for b2 being Gene-Set
for b3, b4 being Individual of b2 holds crossover b3,b4,0,b1 = crossover b4,b3,b1
proof end;

theorem Th8: :: GENEALG1:8
for b1 being Nat
for b2 being Gene-Set
for b3, b4 being Individual of b2 holds crossover b3,b4,b1,0 = crossover b4,b3,b1
proof end;

theorem Th9: :: GENEALG1:9
for b1, b2 being Nat
for b3 being Gene-Set
for b4, b5 being Individual of b3 st b1 >= len b4 holds
crossover b4,b5,b1,b2 = crossover b4,b5,b2
proof end;

theorem Th10: :: GENEALG1:10
for b1, b2 being Nat
for b3 being Gene-Set
for b4, b5 being Individual of b3 st b1 >= len b4 holds
crossover b4,b5,b2,b1 = crossover b4,b5,b2
proof end;

theorem Th11: :: GENEALG1:11
for b1, b2 being Nat
for b3 being Gene-Set
for b4, b5 being Individual of b3 st b1 >= len b4 & b2 >= len b4 holds
crossover b4,b5,b1,b2 = b4
proof end;

theorem Th12: :: GENEALG1:12
for b1 being Nat
for b2 being Gene-Set
for b3, b4 being Individual of b2 holds crossover b3,b4,b1,b1 = b3
proof end;

theorem Th13: :: GENEALG1:13
for b1, b2 being Nat
for b3 being Gene-Set
for b4, b5 being Individual of b3 holds crossover b4,b5,b1,b2 = crossover b4,b5,b2,b1
proof end;

theorem Th14: :: GENEALG1:14
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds crossover b5,b6,b1,b2,b3 is Individual of b4
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4, c5, c6 be Nat;
redefine func crossover as crossover c2,c3,c4,c5,c6 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4,c5,c6 is Individual of c1;
by Th14;
end;

theorem Th15: :: GENEALG1:15
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds
( crossover b5,b6,0,b1,b2 = crossover b6,b5,b1,b2 & crossover b5,b6,b3,0,b2 = crossover b6,b5,b3,b2 & crossover b5,b6,b3,b1,0 = crossover b6,b5,b3,b1 )
proof end;

theorem Th16: :: GENEALG1:16
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds
( crossover b5,b6,0,0,b1 = crossover b5,b6,b1 & crossover b5,b6,b2,0,0 = crossover b5,b6,b2 & crossover b5,b6,0,b3,0 = crossover b5,b6,b3 )
proof end;

theorem Th17: :: GENEALG1:17
for b1 being Gene-Set
for b2, b3 being Individual of b1 holds crossover b2,b3,0,0,0 = b3
proof end;

theorem Th18: :: GENEALG1:18
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 holds
crossover b5,b6,b1,b2,b3 = crossover b5,b6,b2,b3
proof end;

theorem Th19: :: GENEALG1:19
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 holds
crossover b5,b6,b2,b1,b3 = crossover b5,b6,b2,b3
proof end;

theorem Th20: :: GENEALG1:20
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 holds
crossover b5,b6,b2,b3,b1 = crossover b5,b6,b2,b3
proof end;

theorem Th21: :: GENEALG1:21
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 & b2 >= len b5 holds
crossover b5,b6,b1,b2,b3 = crossover b5,b6,b3
proof end;

theorem Th22: :: GENEALG1:22
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 & b2 >= len b5 holds
crossover b5,b6,b1,b3,b2 = crossover b5,b6,b3
proof end;

theorem Th23: :: GENEALG1:23
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 & b2 >= len b5 holds
crossover b5,b6,b3,b1,b2 = crossover b5,b6,b3
proof end;

theorem Th24: :: GENEALG1:24
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 st b1 >= len b5 & b2 >= len b5 & b3 >= len b5 holds
crossover b5,b6,b1,b2,b3 = b5
proof end;

theorem Th25: :: GENEALG1:25
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds
( crossover b5,b6,b1,b2,b3 = crossover b5,b6,b2,b1,b3 & crossover b5,b6,b1,b2,b3 = crossover b5,b6,b1,b3,b2 )
proof end;

theorem Th26: :: GENEALG1:26
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds crossover b5,b6,b1,b2,b3 = crossover b5,b6,b3,b1,b2
proof end;

theorem Th27: :: GENEALG1:27
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds
( crossover b5,b6,b1,b1,b2 = crossover b5,b6,b2 & crossover b5,b6,b1,b3,b1 = crossover b5,b6,b3 & crossover b5,b6,b1,b3,b3 = crossover b5,b6,b1 )
proof end;

theorem Th28: :: GENEALG1:28
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds crossover b6,b7,b1,b2,b3,b4 is Individual of b5
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4, c5, c6, c7 be Nat;
redefine func crossover as crossover c2,c3,c4,c5,c6,c7 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4,c5,c6,c7 is Individual of c1;
by Th28;
end;

theorem Th29: :: GENEALG1:29
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( crossover b6,b7,0,b1,b2,b3 = crossover b7,b6,b1,b2,b3 & crossover b6,b7,b4,0,b2,b3 = crossover b7,b6,b4,b2,b3 & crossover b6,b7,b4,b1,0,b3 = crossover b7,b6,b4,b1,b3 & crossover b6,b7,b4,b1,b2,0 = crossover b7,b6,b4,b1,b2 )
proof end;

theorem Th30: :: GENEALG1:30
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( crossover b6,b7,0,0,b1,b2 = crossover b6,b7,b1,b2 & crossover b6,b7,0,b3,0,b2 = crossover b6,b7,b3,b2 & crossover b6,b7,0,b3,b1,0 = crossover b6,b7,b3,b1 & crossover b6,b7,b4,0,b1,0 = crossover b6,b7,b4,b1 & crossover b6,b7,b4,0,0,b2 = crossover b6,b7,b4,b2 & crossover b6,b7,b4,b3,0,0 = crossover b6,b7,b4,b3 )
proof end;

theorem Th31: :: GENEALG1:31
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( crossover b6,b7,b1,0,0,0 = crossover b7,b6,b1 & crossover b6,b7,0,b2,0,0 = crossover b7,b6,b2 & crossover b6,b7,0,0,b3,0 = crossover b7,b6,b3 & crossover b6,b7,0,0,0,b4 = crossover b7,b6,b4 )
proof end;

theorem Th32: :: GENEALG1:32
for b1 being Gene-Set
for b2, b3 being Individual of b1 holds crossover b2,b3,0,0,0,0 = b2
proof end;

theorem Th33: :: GENEALG1:33
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( ( b1 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b3,b4 ) & ( b2 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b3,b4 ) & ( b3 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b2,b4 ) & ( b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b2,b3 ) )
proof end;

theorem Th34: :: GENEALG1:34
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( ( b1 >= len b6 & b2 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b4 ) & ( b1 >= len b6 & b3 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b4 ) & ( b1 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b3 ) & ( b2 >= len b6 & b3 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b4 ) & ( b2 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b3 ) & ( b3 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b2 ) )
proof end;

theorem Th35: :: GENEALG1:35
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( ( b1 >= len b6 & b2 >= len b6 & b3 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4 ) & ( b1 >= len b6 & b2 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3 ) & ( b1 >= len b6 & b3 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2 ) & ( b2 >= len b6 & b3 >= len b6 & b4 >= len b6 implies crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1 ) )
proof end;

theorem Th36: :: GENEALG1:36
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 st b1 >= len b6 & b2 >= len b6 & b3 >= len b6 & b4 >= len b6 holds
crossover b6,b7,b1,b2,b3,b4 = b6
proof end;

theorem Th37: :: GENEALG1:37
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b2,b4,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b3,b2,b4 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b3,b4,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b4,b2,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b1,b4,b3,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b1,b3,b4 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b1,b4,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b3,b1,b4 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b3,b4,b1 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b4,b1,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b2,b4,b3,b1 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b1,b2,b4 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b1,b4,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b2,b1,b4 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b2,b4,b1 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b4,b1,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b3,b4,b2,b1 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b1,b2,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b1,b3,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b2,b1,b3 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b2,b3,b1 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b3,b1,b2 & crossover b6,b7,b1,b2,b3,b4 = crossover b6,b7,b4,b3,b2,b1 )
proof end;

theorem Th38: :: GENEALG1:38
for b1, b2, b3, b4 being Nat
for b5 being Gene-Set
for b6, b7 being Individual of b5 holds
( crossover b6,b7,b1,b1,b2,b3 = crossover b6,b7,b2,b3 & crossover b6,b7,b1,b4,b1,b3 = crossover b6,b7,b4,b3 & crossover b6,b7,b1,b4,b2,b1 = crossover b6,b7,b4,b2 & crossover b6,b7,b1,b4,b4,b3 = crossover b6,b7,b1,b3 & crossover b6,b7,b1,b4,b2,b4 = crossover b6,b7,b1,b2 & crossover b6,b7,b1,b4,b2,b2 = crossover b6,b7,b1,b4 )
proof end;

theorem Th39: :: GENEALG1:39
for b1, b2, b3 being Nat
for b4 being Gene-Set
for b5, b6 being Individual of b4 holds
( crossover b5,b6,b1,b1,b2,b2 = b5 & crossover b5,b6,b1,b3,b1,b3 = b5 & crossover b5,b6,b1,b3,b3,b1 = b5 )
proof end;

theorem Th40: :: GENEALG1:40
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds crossover b7,b8,b1,b2,b3,b4,b5 is Individual of b6
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4, c5, c6, c7, c8 be Nat;
redefine func crossover as crossover c2,c3,c4,c5,c6,c7,c8 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4,c5,c6,c7,c8 is Individual of c1;
by Th40;
end;

theorem Th41: :: GENEALG1:41
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,0,b1,b2,b3,b4 = crossover b8,b7,b1,b2,b3,b4 & crossover b7,b8,b5,0,b2,b3,b4 = crossover b8,b7,b5,b2,b3,b4 & crossover b7,b8,b5,b1,0,b3,b4 = crossover b8,b7,b5,b1,b3,b4 & crossover b7,b8,b5,b1,b2,0,b4 = crossover b8,b7,b5,b1,b2,b4 & crossover b7,b8,b5,b1,b2,b3,0 = crossover b8,b7,b5,b1,b2,b3 )
proof end;

theorem Th42: :: GENEALG1:42
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,0,0,b1,b2,b3 = crossover b7,b8,b1,b2,b3 & crossover b7,b8,0,b4,0,b2,b3 = crossover b7,b8,b4,b2,b3 & crossover b7,b8,0,b4,b1,0,b3 = crossover b7,b8,b4,b1,b3 & crossover b7,b8,0,b4,b1,b2,0 = crossover b7,b8,b4,b1,b2 & crossover b7,b8,b5,0,0,b2,b3 = crossover b7,b8,b5,b2,b3 & crossover b7,b8,b5,0,b1,0,b3 = crossover b7,b8,b5,b1,b3 & crossover b7,b8,b5,0,b1,b2,0 = crossover b7,b8,b5,b1,b2 & crossover b7,b8,b5,b4,0,0,b3 = crossover b7,b8,b5,b4,b3 & crossover b7,b8,b5,b4,0,b2,0 = crossover b7,b8,b5,b4,b2 & crossover b7,b8,b5,b4,b1,0,0 = crossover b7,b8,b5,b4,b1 )
proof end;

theorem Th43: :: GENEALG1:43
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,0,0,0,b1,b2 = crossover b8,b7,b1,b2 & crossover b7,b8,0,0,b3,0,b2 = crossover b8,b7,b3,b2 & crossover b7,b8,0,0,b3,b1,0 = crossover b8,b7,b3,b1 & crossover b7,b8,0,b4,0,0,b2 = crossover b8,b7,b4,b2 & crossover b7,b8,0,b4,0,b1,0 = crossover b8,b7,b4,b1 & crossover b7,b8,0,b4,b3,0,0 = crossover b8,b7,b4,b3 & crossover b7,b8,b5,0,0,0,b2 = crossover b8,b7,b5,b2 & crossover b7,b8,b5,0,0,b1,0 = crossover b8,b7,b5,b1 & crossover b7,b8,b5,0,b3,0,0 = crossover b8,b7,b5,b3 & crossover b7,b8,b5,b4,0,0,0 = crossover b8,b7,b5,b4 )
proof end;

theorem Th44: :: GENEALG1:44
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,0,0,0,0,b1 = crossover b7,b8,b1 & crossover b7,b8,0,0,0,b2,0 = crossover b7,b8,b2 & crossover b7,b8,0,0,b3,0,0 = crossover b7,b8,b3 & crossover b7,b8,0,b4,0,0,0 = crossover b7,b8,b4 & crossover b7,b8,b5,0,0,0,0 = crossover b7,b8,b5 )
proof end;

theorem Th45: :: GENEALG1:45
for b1 being Gene-Set
for b2, b3 being Individual of b1 holds crossover b2,b3,0,0,0,0,0 = b3
proof end;

theorem Th46: :: GENEALG1:46
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( ( b1 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b3,b4,b5 ) & ( b2 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b3,b4,b5 ) & ( b3 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b4,b5 ) & ( b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b3,b5 ) & ( b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b3,b4 ) )
proof end;

theorem Th47: :: GENEALG1:47
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( ( b1 >= len b7 & b2 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b3,b4,b5 ) & ( b1 >= len b7 & b3 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b4,b5 ) & ( b1 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b3,b5 ) & ( b1 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b3,b4 ) & ( b2 >= len b7 & b3 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b4,b5 ) & ( b2 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b3,b5 ) & ( b2 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b3,b4 ) & ( b3 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b5 ) & ( b3 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b4 ) & ( b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2,b3 ) )
proof end;

theorem Th48: :: GENEALG1:48
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( ( b1 >= len b7 & b2 >= len b7 & b3 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b4,b5 ) & ( b1 >= len b7 & b2 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b3,b5 ) & ( b1 >= len b7 & b2 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b3,b4 ) & ( b1 >= len b7 & b3 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b5 ) & ( b1 >= len b7 & b3 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b4 ) & ( b1 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b3 ) & ( b2 >= len b7 & b3 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b5 ) & ( b2 >= len b7 & b3 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b4 ) & ( b2 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b3 ) & ( b3 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1,b2 ) )
proof end;

theorem Th49: :: GENEALG1:49
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( ( b1 >= len b7 & b2 >= len b7 & b3 >= len b7 & b4 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b5 ) & ( b1 >= len b7 & b2 >= len b7 & b3 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b4 ) & ( b1 >= len b7 & b2 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b3 ) & ( b1 >= len b7 & b3 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2 ) & ( b2 >= len b7 & b3 >= len b7 & b4 >= len b7 & b5 >= len b7 implies crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b1 ) )
proof end;

theorem Th50: :: GENEALG1:50
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 st b1 >= len b7 & b2 >= len b7 & b3 >= len b7 & b4 >= len b7 & b5 >= len b7 holds
crossover b7,b8,b1,b2,b3,b4,b5 = b7
proof end;

theorem Th51: :: GENEALG1:51
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b2,b1,b3,b4,b5 & crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b3,b2,b1,b4,b5 & crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b4,b2,b3,b1,b5 & crossover b7,b8,b1,b2,b3,b4,b5 = crossover b7,b8,b5,b2,b3,b4,b1 )
proof end;

theorem Th52: :: GENEALG1:52
for b1, b2, b3, b4, b5 being Nat
for b6 being Gene-Set
for b7, b8 being Individual of b6 holds
( crossover b7,b8,b1,b1,b2,b3,b4 = crossover b7,b8,b2,b3,b4 & crossover b7,b8,b1,b5,b1,b3,b4 = crossover b7,b8,b5,b3,b4 & crossover b7,b8,b1,b5,b2,b1,b4 = crossover b7,b8,b5,b2,b4 & crossover b7,b8,b1,b5,b2,b3,b1 = crossover b7,b8,b5,b2,b3 )
proof end;

theorem Th53: :: GENEALG1:53
for b1, b2, b3, b4, b5, b6 being Nat
for b7 being Gene-Set
for b8, b9 being Individual of b7 holds crossover b8,b9,b1,b2,b3,b4,b5,b6 is Individual of b7
proof end;

definition
let c1 be Gene-Set;
let c2, c3 be Individual of c1;
let c4, c5, c6, c7, c8, c9 be Nat;
redefine func crossover as crossover c2,c3,c4,c5,c6,c7,c8,c9 -> Individual of a1;
correctness
coherence
crossover c2,c3,c4,c5,c6,c7,c8,c9 is Individual of c1;
by Th53;
end;

theorem Th54: :: GENEALG1:54
for b1, b2, b3, b4, b5, b6 being Nat
for b7 being Gene-Set
for b8, b9 being Individual of b7 holds
( crossover b8,b9,0,b1,b2,b3,b4,b5 = crossover b9,b8,b1,b2,b3,b4,b5 & crossover b8,b9,b6,0,b2,b3,b4,b5 = crossover b9,b8,b6,b2,b3,b4,b5 & crossover b8,b9,b6,b1,0,b3,b4,b5 = crossover b9,b8,b6,b1,b3,b4,b5 & crossover b8,b9,b6,b1,b2,0,b4,b5 = crossover b9,b8,b6,b1,b2,b4,b5 & crossover b8,b9,b6,b1,b2,b3,0,b5 = crossover b9,b8,b6,b1,b2,b3,b5 & crossover b8,b9,b6,b1,b2,b3,b4,0 = crossover b9,b8,b6,b1,b2,b3,b4 )
proof end;

theorem Th55: :: GENEALG1:55
for b1, b2, b3, b4, b5, b6 being Nat
for b7 being Gene-Set
for b8, b9 being Individual of b7 holds
( ( b1 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b2,b3,b4,b5,b6 ) & ( b2 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b1,b3,b4,b5,b6 ) & ( b3 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b1,b2,b4,b5,b6 ) & ( b4 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b1,b2,b3,b5,b6 ) & ( b5 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b1,b2,b3,b4,b6 ) & ( b6 >= len b8 implies crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b1,b2,b3,b4,b5 ) )
proof end;

theorem Th56: :: GENEALG1:56
for b1, b2, b3, b4, b5, b6 being Nat
for b7 being Gene-Set
for b8, b9 being Individual of b7 holds
( crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b2,b1,b3,b4,b5,b6 & crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b3,b2,b1,b4,b5,b6 & crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b4,b2,b3,b1,b5,b6 & crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b5,b2,b3,b4,b1,b6 & crossover b8,b9,b1,b2,b3,b4,b5,b6 = crossover b8,b9,b6,b2,b3,b4,b5,b1 )
proof end;

theorem Th57: :: GENEALG1:57
for b1, b2, b3, b4, b5, b6 being Nat
for b7 being Gene-Set
for b8, b9 being Individual of b7 holds
( crossover b8,b9,b1,b1,b2,b3,b4,b5 = crossover b8,b9,b2,b3,b4,b5 & crossover b8,b9,b1,b6,b1,b3,b4,b5 = crossover b8,b9,b6,b3,b4,b5 & crossover b8,b9,b1,b6,b2,b1,b4,b5 = crossover b8,b9,b6,b2,b4,b5 & crossover b8,b9,b1,b6,b2,b3,b1,b5 = crossover b8,b9,b6,b2,b3,b5 & crossover b8,b9,b1,b6,b2,b3,b4,b1 = crossover b8,b9,b6,b2,b3,b4 )
proof end;