let n1, n2, n3, n4, n5 be Element of NAT ; for S being Gene-Set
for p1, p2 being Individual of S holds
( crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n1,n3,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n2,n1,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n2,n3,n1,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1) )
let S be Gene-Set; for p1, p2 being Individual of S holds
( crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n1,n3,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n2,n1,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n2,n3,n1,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1) )
let p1, p2 be Individual of S; ( crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n1,n3,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n2,n1,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n2,n3,n1,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1) )
A1: crossover (p1,p2,n1,n2,n3,n4,n5) =
crossover ((crossover (p1,p2,n3,n2,n1,n4)),(crossover (p2,p1,n1,n2,n3,n4)),n5)
by Th37
.=
crossover ((crossover (p1,p2,n3,n2,n1,n4)),(crossover (p2,p1,n3,n2,n1,n4)),n5)
by Th37
;
A2: crossover (p1,p2,n1,n2,n3,n4,n5) =
crossover ((crossover (p1,p2,n4,n2,n3,n1)),(crossover (p2,p1,n1,n2,n3,n4)),n5)
by Th37
.=
crossover ((crossover (p1,p2,n4,n2,n3,n1)),(crossover (p2,p1,n4,n2,n3,n1)),n5)
by Th37
;
A3:
crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1)
proof
set q2 =
crossover (
p2,
p1,
n2,
n3,
n4);
set q1 =
crossover (
p1,
p2,
n2,
n3,
n4);
A4:
crossover (
p1,
p2,
n2,
n3,
n4,
n5)
= crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n5)
;
crossover (
p1,
p2,
n1,
n2,
n3,
n4,
n5) =
crossover (
(crossover (p1,p2,n2,n3,n4,n1)),
(crossover (p2,p1,n1,n2,n3,n4)),
n5)
by Th37
.=
crossover (
(crossover (p1,p2,n2,n3,n4,n1)),
(crossover (p2,p1,n2,n3,n4,n1)),
n5)
by Th37
.=
crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n1,
n5)
.=
crossover (
(crossover (p1,p2,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4)),
n5,
n1)
by Th13
.=
crossover (
(crossover (p1,p2,n5,n2,n3,n4)),
(crossover (p2,p1,n2,n3,n4,n5)),
n1)
by A4, Th37
.=
crossover (
(crossover (p1,p2,n5,n2,n3,n4)),
(crossover (p2,p1,n5,n2,n3,n4)),
n1)
by Th37
;
hence
crossover (
p1,
p2,
n1,
n2,
n3,
n4,
n5)
= crossover (
p1,
p2,
n5,
n2,
n3,
n4,
n1)
;
verum
end;
crossover (p1,p2,n1,n2,n3,n4,n5) =
crossover ((crossover (p1,p2,n2,n1,n3,n4)),(crossover (p2,p1,n1,n2,n3,n4)),n5)
by Th37
.=
crossover ((crossover (p1,p2,n2,n1,n3,n4)),(crossover (p2,p1,n2,n1,n3,n4)),n5)
by Th37
;
hence
( crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n2,n1,n3,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n3,n2,n1,n4,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n4,n2,n3,n1,n5) & crossover (p1,p2,n1,n2,n3,n4,n5) = crossover (p1,p2,n5,n2,n3,n4,n1) )
by A1, A2, A3; verum