let n1, n2, n3, n4, n5 be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 p1,p2,n2,n1,n3,n4,n5
proof
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
;
:: thesis: verum
end;
A2:
crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n3,n2,n1,n4,n5
proof
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
;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 = crossover p1,
p2,
n3,
n2,
n1,
n4,
n5
;
:: thesis: verum
end;
A3:
crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n4,n2,n3,n1,n5
proof
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
;
hence
crossover p1,
p2,
n1,
n2,
n3,
n4,
n5 = crossover p1,
p2,
n4,
n2,
n3,
n1,
n5
;
:: thesis: verum
end;
crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n5,n2,n3,n4,n1
proof
set q1 =
crossover p1,
p2,
n2,
n3,
n4;
set q2 =
crossover p2,
p1,
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
;
:: thesis: verum
end;
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; :: thesis: verum