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