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 & 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) ) )
let S be 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) ) )
let p1, p2 be Individual of S; ( ( 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) ) )
A1:
( n1 >= len p1 & n2 >= len p1 & n3 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4) )
proof
assume that A2:
(
n1 >= len p1 &
n2 >= len p1 )
and A3:
n3 >= len p1
;
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4)
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n3,
n4)
by A2, Th34;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n4)
by A3, Th9;
verum
end;
A4:
( n1 >= len p1 & n3 >= len p1 & n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2) )
proof
assume that A5:
(
n1 >= len p1 &
n3 >= len p1 )
and A6:
n4 >= len p1
;
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2)
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
p1,
p2,
n2,
n4)
by A5, Th34
.=
crossover (
p1,
p2,
n4,
n2)
by Th13
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n2)
by A6, Th9;
verum
end;
A7:
( n2 >= len p1 & n3 >= len p1 & n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1) )
proof
assume that A8:
(
n2 >= len p1 &
n3 >= len p1 )
and A9:
n4 >= len p1
;
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1)
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
p1,
p2,
n1,
n4)
by A8, Th34
.=
crossover (
p1,
p2,
n4,
n1)
by Th13
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n1)
by A9, Th9;
verum
end;
( n1 >= len p1 & n2 >= len p1 & n4 >= len p1 implies crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3) )
proof
assume that A10:
(
n1 >= len p1 &
n2 >= len p1 )
and A11:
n4 >= len p1
;
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3)
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
p1,
p2,
n3,
n4)
by A10, Th34
.=
crossover (
p1,
p2,
n4,
n3)
by Th13
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n3)
by A11, Th9;
verum
end;
hence
( ( 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) ) )
by A1, A4, A7; verum