:: GENEALG1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: GENEALG1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th2: :: GENEALG1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f1, f2 being FinSequence of D
for i being Nat holds (f1 ^ f2) | ((len f1) + i) = f1 ^ (f2 | i)
proof end;

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
proof end;
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 & ( for i being 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 & ( for i being Nat st i in dom b1 holds
b1 . i in S . i ) )
proof end;
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 & ( for i being Nat st i in dom b2 holds
b2 . i in S . i ) ) );

definition
let S be Gene-Set;
let p1, p2 be FinSequence of GA-Space S;
let n be 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 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 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 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 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 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 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 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 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 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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Gene-Set
for p1, p2 being Individual of S holds crossover p1,p2,0 = p2
proof end;

theorem Th5: :: GENEALG1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being 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
proof end;

theorem Th10: :: GENEALG1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n1 being 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
proof end;

theorem :: GENEALG1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being 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
proof end;

theorem Th12: :: GENEALG1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1 being Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2 being Nat
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being Nat
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n3, n1 being 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 )
proof end;

theorem :: GENEALG1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n3, n1, n2 being 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 )
proof end;

theorem :: GENEALG1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Gene-Set
for p1, p2 being Individual of S holds crossover p1,p2,0,0,0 = p2
proof end;

theorem Th18: :: GENEALG1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being 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
proof end;

theorem Th19: :: GENEALG1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n1, n3 being 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
proof end;

theorem Th20: :: GENEALG1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n3, n1, n2 being 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
proof end;

theorem Th21: :: GENEALG1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being 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
proof end;

theorem :: GENEALG1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n2 being 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
proof end;

theorem :: GENEALG1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n3, n1 being 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
proof end;

theorem :: GENEALG1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being 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
proof end;

theorem Th25: :: GENEALG1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being 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 )
proof end;

theorem Th26: :: GENEALG1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3 being 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
proof end;

theorem Th27: :: GENEALG1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n2 being 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 )
proof end;

theorem Th28: :: GENEALG1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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
proof end;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3, n4 be 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n3, n4, n1 being 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 )
proof end;

theorem Th30: :: GENEALG1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n3, n4, n2, n1 being 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 )
proof end;

theorem Th31: :: GENEALG1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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 )
proof end;

theorem Th32: :: GENEALG1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Gene-Set
for p1, p2 being Individual of S holds crossover p1,p2,0,0,0,0 = p1
proof end;

theorem Th33: :: GENEALG1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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 ) )
proof end;

theorem Th34: :: GENEALG1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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 ) )
proof end;

theorem Th35: :: GENEALG1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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 ) )
proof end;

theorem Th36: :: GENEALG1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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
proof end;

theorem Th37: :: GENEALG1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4 being 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,n2,n3 & 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,n1,n2,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n1,n4,n2 & 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,n1,n2,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n1,n3,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n1,n3 & 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,n1,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 )
proof end;

theorem Th38: :: GENEALG1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n4, n2 being 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 )
proof end;

theorem :: GENEALG1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n2 being 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 )
proof end;

theorem Th40: :: GENEALG1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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
proof end;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3, n4, n5 be 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n3, n4, n5, n1 being 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 )
proof end;

theorem :: GENEALG1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n3, n4, n5, n2, n1 being 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 )
proof end;

theorem :: GENEALG1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n4, n5, n3, n2, n1 being 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 )
proof end;

theorem :: GENEALG1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n5, n4, n3, n2, n1 being 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 )
proof end;

theorem :: GENEALG1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Gene-Set
for p1, p2 being Individual of S holds crossover p1,p2,0,0,0,0,0 = p2
proof end;

theorem Th46: :: GENEALG1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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 ) )
proof end;

theorem :: GENEALG1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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 ) )
proof end;

theorem :: GENEALG1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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 ) )
proof end;

theorem :: GENEALG1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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 ) )
proof end;

theorem :: GENEALG1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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
proof end;

theorem Th51: :: GENEALG1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5 being 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 )
proof end;

theorem Th52: :: GENEALG1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n4, n5, n2 being 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 )
proof end;

theorem Th53: :: GENEALG1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5, n6 being 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
proof end;

definition
let S be Gene-Set;
let p1, p2 be Individual of S;
let n1, n2, n3, n4, n5, n6 be 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n2, n3, n4, n5, n6, n1 being 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 )
proof end;

theorem :: GENEALG1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5, n6 being 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 ) )
proof end;

theorem Th56: :: GENEALG1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n2, n3, n4, n5, n6 being 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 )
proof end;

theorem :: GENEALG1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n1, n3, n4, n5, n6, n2 being 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 )
proof end;