let n1, n2, n3, n4 be 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 ) )
let S be 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 ) )
let p1, p2 be Individual of S; ( ( 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 ) )
A1:
( n1 >= len p1 & n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4 )
proof
assume that A2:
n1 >= len p1
and A3:
n3 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n2,
n3,
n4
by A2, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n2,
n4
by A3, Th19;
verum
end;
A4:
( n1 >= len p1 & n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3 )
proof
assume that A5:
n1 >= len p1
and A6:
n4 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n2,
n3,
n4
by A5, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n2,
n3
by A6, Th20;
verum
end;
A7:
( n3 >= len p1 & n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2 )
proof
assume that A8:
n3 >= len p1
and A9:
n4 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n2,
n4
by A8, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n2
by A9, Th20;
verum
end;
A10:
( n2 >= len p1 & n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3 )
proof
assume that A11:
n2 >= len p1
and A12:
n4 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n3,
n4
by A11, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n3
by A12, Th20;
verum
end;
A13:
( n2 >= len p1 & n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4 )
proof
assume that A14:
n2 >= len p1
and A15:
n3 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n3,
n4
by A14, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n1,
n4
by A15, Th19;
verum
end;
( n1 >= len p1 & n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4 )
proof
assume that A16:
n1 >= len p1
and A17:
n2 >= len p1
;
crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n2,
n3,
n4
by A16, Th33;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4 = crossover p1,
p2,
n3,
n4
by A17, Th18;
verum
end;
hence
( ( 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 ) )
by A1, A4, A13, A10, A7; verum