let n1, n2, n3, n4 be Element of 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,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,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,n2,n3,n1) & crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1) )
let S be 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,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,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,n2,n3,n1) & crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1) )
let p1, p2 be Individual of S; ( 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,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,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,n2,n3,n1) & crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1) )
A1:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n2,n4,n3)
proof
set q2 =
crossover (
p2,
p1,
n1,
n2);
set q1 =
crossover (
p1,
p2,
n1,
n2);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n1,n2)),
(crossover (p2,p1,n1,n2)),
n3,
n4)
.=
crossover (
(crossover (p1,p2,n1,n2)),
(crossover (p2,p1,n1,n2)),
n4,
n3)
by Th13
.=
crossover (
(crossover ((crossover (p1,p2,n1,n2)),(crossover (p2,p1,n1,n2)),n4)),
(crossover ((crossover (p2,p1,n1,n2)),(crossover (p1,p2,n1,n2)),n4)),
n3)
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n1,
n2,
n4,
n3)
;
verum
end;
A2: crossover (p1,p2,n1,n2,n3,n4) =
crossover ((crossover (p1,p2,n1,n3,n2)),(crossover (p2,p1,n1,n2,n3)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n1,n3,n2)),(crossover (p2,p1,n1,n3,n2)),n4)
by Th25
;
A3:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n3,n4,n1)
proof
set q2 =
crossover (
p2,
p1,
n2,
n3);
set q1 =
crossover (
p1,
p2,
n2,
n3);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n3,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n1)
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n2,
n3,
n4,
n1)
;
verum
end;
A4:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n4,n3,n2)
proof
set q2 =
crossover (
p2,
p1,
n1,
n3);
set q1 =
crossover (
p1,
p2,
n1,
n3);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n1,n3,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n1,n3,n2)),
(crossover (p2,p1,n1,n3,n2)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n1,n3)),
(crossover (p2,p1,n1,n3)),
n2,
n4)
.=
crossover (
(crossover (p1,p2,n1,n3)),
(crossover (p2,p1,n1,n3)),
n4,
n2)
by Th13
.=
crossover (
(crossover (p1,p2,n1,n3,n4)),
(crossover (p2,p1,n1,n3,n4)),
n2)
.=
crossover (
(crossover (p1,p2,n1,n4,n3)),
(crossover (p2,p1,n1,n3,n4)),
n2)
by Th25
.=
crossover (
(crossover (p1,p2,n1,n4,n3)),
(crossover (p2,p1,n1,n4,n3)),
n2)
by Th25
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n1,
n4,
n3,
n2)
;
verum
end;
A5:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1)
proof
set q2 =
crossover (
p2,
p1,
n3,
n2);
set q1 =
crossover (
p1,
p2,
n3,
n2);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n2,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n3,n2,n4)),
(crossover (p2,p1,n3,n2,n4)),
n1)
.=
crossover (
(crossover (p1,p2,n4,n3,n2)),
(crossover (p2,p1,n3,n2,n4)),
n1)
by Th26
.=
crossover (
(crossover (p1,p2,n4,n3,n2)),
(crossover (p2,p1,n4,n3,n2)),
n1)
by Th26
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n4,
n3,
n2,
n1)
;
verum
end;
A6:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n1,n4,n3)
proof
set q2 =
crossover (
p2,
p1,
n2,
n1);
set q1 =
crossover (
p1,
p2,
n2,
n1);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n1)),
(crossover (p2,p1,n2,n1)),
n3,
n4)
.=
crossover (
(crossover (p1,p2,n2,n1)),
(crossover (p2,p1,n2,n1)),
n4,
n3)
by Th13
.=
crossover (
(crossover (p1,p2,n2,n1,n4)),
(crossover (p2,p1,n2,n1,n4)),
n3)
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n2,
n1,
n4,
n3)
;
verum
end;
A7:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n2,n3,n1)
proof
set q2 =
crossover (
p2,
p1,
n2,
n3);
set q1 =
crossover (
p1,
p2,
n2,
n3);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n3,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n1)
.=
crossover (
(crossover (p1,p2,n4,n2,n3)),
(crossover (p2,p1,n2,n3,n4)),
n1)
by Th26
.=
crossover (
(crossover (p1,p2,n4,n2,n3)),
(crossover (p2,p1,n4,n2,n3)),
n1)
by Th26
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n4,
n2,
n3,
n1)
;
verum
end;
A8:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n1,n3,n4,n2)
proof
set q2 =
crossover (
p2,
p1,
n1,
n3);
set q1 =
crossover (
p1,
p2,
n1,
n3);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n1,n3,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n1,n3,n2)),
(crossover (p2,p1,n1,n3,n2)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n1,n3)),
(crossover (p2,p1,n1,n3)),
n2,
n4)
.=
crossover (
(crossover (p1,p2,n1,n3)),
(crossover (p2,p1,n1,n3)),
n4,
n2)
by Th13
.=
crossover (
(crossover ((crossover (p1,p2,n1,n3)),(crossover (p2,p1,n1,n3)),n4)),
(crossover ((crossover (p2,p1,n1,n3)),(crossover (p1,p2,n1,n3)),n4)),
n2)
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n1,
n3,
n4,
n2)
;
verum
end;
A9:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n2,n4,n1)
proof
set q2 =
crossover (
p2,
p1,
n3,
n2);
set q1 =
crossover (
p1,
p2,
n3,
n2);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n2,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n3,n2,n4)),
(crossover (p2,p1,n3,n2,n4)),
n1)
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n3,
n2,
n4,
n1)
;
verum
end;
A10:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n4,n1,n3)
proof
set q2 =
crossover (
p2,
p1,
n2,
n1);
set q1 =
crossover (
p1,
p2,
n2,
n1);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n1)),
(crossover (p2,p1,n2,n1)),
n3,
n4)
.=
crossover (
(crossover (p1,p2,n2,n1)),
(crossover (p2,p1,n2,n1)),
n4,
n3)
by Th13
.=
crossover (
(crossover (p1,p2,n2,n1,n4)),
(crossover (p2,p1,n2,n1,n4)),
n3)
.=
crossover (
(crossover (p1,p2,n2,n4,n1)),
(crossover (p2,p1,n2,n1,n4)),
n3)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n4,n1)),
(crossover (p2,p1,n2,n4,n1)),
n3)
by Th25
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n2,
n4,
n1,
n3)
;
verum
end;
A11:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n4,n2,n1)
proof
set q2 =
crossover (
p2,
p1,
n3,
n2);
set q1 =
crossover (
p1,
p2,
n3,
n2);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2,n1)),
(crossover (p2,p1,n3,n2,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n3,n2)),
(crossover (p2,p1,n3,n2)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n3,n2,n4)),
(crossover (p2,p1,n3,n2,n4)),
n1)
.=
crossover (
(crossover (p1,p2,n3,n4,n2)),
(crossover (p2,p1,n3,n2,n4)),
n1)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n4,n2)),
(crossover (p2,p1,n3,n4,n2)),
n1)
by Th25
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n3,
n4,
n2,
n1)
;
verum
end;
A12: crossover (p1,p2,n1,n2,n3,n4) =
crossover ((crossover (p1,p2,n3,n1,n2)),(crossover (p2,p1,n1,n2,n3)),n4)
by Th26
.=
crossover ((crossover (p1,p2,n3,n1,n2)),(crossover (p2,p1,n3,n1,n2)),n4)
by Th26
.=
crossover ((crossover (p1,p2,n3,n2,n1)),(crossover (p2,p1,n3,n1,n2)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n3,n2,n1)),(crossover (p2,p1,n3,n2,n1)),n4)
by Th25
;
A13:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n3,n4,n1,n2)
proof
set q2 =
crossover (
p2,
p1,
n3,
n1);
set q1 =
crossover (
p1,
p2,
n3,
n1);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n1,n2)),
(crossover (p2,p1,n3,n1,n2)),
n4)
by Th26
.=
crossover (
(crossover (p1,p2,n3,n1)),
(crossover (p2,p1,n3,n1)),
n2,
n4)
.=
crossover (
(crossover (p1,p2,n3,n1)),
(crossover (p2,p1,n3,n1)),
n4,
n2)
by Th13
.=
crossover (
(crossover (p1,p2,n3,n1,n4)),
(crossover (p2,p1,n3,n1,n4)),
n2)
.=
crossover (
(crossover (p1,p2,n3,n4,n1)),
(crossover (p2,p1,n3,n1,n4)),
n2)
by Th25
.=
crossover (
(crossover (p1,p2,n3,n4,n1)),
(crossover (p2,p1,n3,n4,n1)),
n2)
by Th25
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n3,
n4,
n1,
n2)
;
verum
end;
A14:
crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n2,n4,n3,n1)
proof
set q2 =
crossover (
p2,
p1,
n2,
n3);
set q1 =
crossover (
p1,
p2,
n2,
n3);
crossover (
p1,
p2,
n1,
n2,
n3,
n4) =
crossover (
(crossover (p1,p2,n2,n1,n3)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n1,n2,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n1,n3)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3,n1)),
(crossover (p2,p1,n2,n3,n1)),
n4)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n1,
n4)
.=
crossover (
(crossover (p1,p2,n2,n3)),
(crossover (p2,p1,n2,n3)),
n4,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n1)
.=
crossover (
(crossover (p1,p2,n2,n4,n3)),
(crossover (p2,p1,n2,n3,n4)),
n1)
by Th25
.=
crossover (
(crossover (p1,p2,n2,n4,n3)),
(crossover (p2,p1,n2,n4,n3)),
n1)
by Th25
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4)
= crossover (
p1,
p2,
n2,
n4,
n3,
n1)
;
verum
end;
A15: crossover (p1,p2,n1,n2,n3,n4) =
crossover ((crossover (p1,p2,n2,n1,n3)),(crossover (p2,p1,n1,n2,n3)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n2,n1,n3)),(crossover (p2,p1,n2,n1,n3)),n4)
by Th25
;
crossover (p1,p2,n1,n2,n3,n4) =
crossover ((crossover (p1,p2,n2,n1,n3)),(crossover (p2,p1,n1,n2,n3)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n2,n1,n3)),(crossover (p2,p1,n2,n1,n3)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n2,n3,n1)),(crossover (p2,p1,n2,n1,n3)),n4)
by Th25
.=
crossover ((crossover (p1,p2,n2,n3,n1)),(crossover (p2,p1,n2,n3,n1)),n4)
by Th25
;
hence
( 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,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,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,n2,n3,n1) & crossover (p1,p2,n1,n2,n3,n4) = crossover (p1,p2,n4,n3,n2,n1) )
by A2, A15, A1, A8, A4, A6, A3, A10, A14, A12, A9, A13, A11, A7, A5; verum