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