:: GENEALG1 semantic presentation begin theorem :: GENEALG1:1 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1"))))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" ) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2"))))))) ; theorem :: GENEALG1:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f2")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" )))))) ; definitionmode Gene-Set is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::); end; notationlet "S" be ($#m1_hidden :::"Gene-Set":::); synonym :::"GA-Space"::: "S" for :::"Union"::: "S"; end; registrationlet "f" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k3_card_3 :::"GA-Space"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); mode :::"Individual"::: "of" "S" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") means :: GENEALG1:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "S")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set "S" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ); end; :: deftheorem defines :::"Individual"::: GENEALG1:def 1 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ))); begin definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 2 (Set (Set "(" "p1" ($#k17_finseq_1 :::"|"::: ) "n" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" "p2" ($#k2_rfinseq :::"/^"::: ) "n" ")" )); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p1")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "p2")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")) ")" )))))); definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n1", "n2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 3 (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k1_genealg1 :::"crossover"::: ) "(" "p1" "," "p2" "," "n1" ")" ")" ) "," (Set "(" ($#k1_genealg1 :::"crossover"::: ) "(" "p2" "," "p1" "," "n1" ")" ")" ) "," "n2" ")" ); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k1_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" ")" ) "," (Set "(" ($#k1_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) ")" ")" ) "," (Set (Var "n2")) ")" ))))); definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n1", "n2", "n3" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 4 (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k2_genealg1 :::"crossover"::: ) "(" "p1" "," "p2" "," "n1" "," "n2" ")" ")" ) "," (Set "(" ($#k2_genealg1 :::"crossover"::: ) "(" "p2" "," "p1" "," "n1" "," "n2" ")" ")" ) "," "n3" ")" ); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k2_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" ) "," (Set "(" ($#k2_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ")" ) "," (Set (Var "n3")) ")" ))))); definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n1", "n2", "n3", "n4" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 5 (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k3_genealg1 :::"crossover"::: ) "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" ")" ")" ) "," (Set "(" ($#k3_genealg1 :::"crossover"::: ) "(" "p2" "," "p1" "," "n1" "," "n2" "," "n3" ")" ")" ) "," "n4" ")" ); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k3_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ")" ) "," (Set "(" ($#k3_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ")" ) "," (Set (Var "n4")) ")" ))))); definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n1", "n2", "n3", "n4", "n5" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 6 (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k4_genealg1 :::"crossover"::: ) "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" ")" ")" ) "," (Set "(" ($#k4_genealg1 :::"crossover"::: ) "(" "p2" "," "p1" "," "n1" "," "n2" "," "n3" "," "n4" ")" ")" ) "," "n5" ")" ); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k4_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ")" ) "," (Set "(" ($#k4_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ")" ) "," (Set (Var "n5")) ")" ))))); definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Const "S"))); let "n1", "n2", "n3", "n4", "n5", "n6" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" "," "n6" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) "S") equals :: GENEALG1:def 7 (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k5_genealg1 :::"crossover"::: ) "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" ")" ")" ) "," (Set "(" ($#k5_genealg1 :::"crossover"::: ) "(" "p2" "," "p1" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" ")" ")" ) "," "n6" ")" ); end; :: deftheorem defines :::"crossover"::: GENEALG1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_card_3 :::"GA-Space"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set "(" ($#k5_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ")" ) "," (Set "(" ($#k5_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ")" ) "," (Set (Var "n6")) ")" ))))); begin theorem :: GENEALG1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:4 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: GENEALG1:5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; begin theorem :: GENEALG1:6 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n1", "n2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n")) ")" ))))) ; theorem :: GENEALG1:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n")) ")" ))))) ; theorem :: GENEALG1:9 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" ))))) ; theorem :: GENEALG1:10 (Bool "for" (Set (Var "n2")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" ))))) ; theorem :: GENEALG1:11 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; theorem :: GENEALG1:12 (Bool "for" (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; theorem :: GENEALG1:13 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) ")" ))))) ; begin theorem :: GENEALG1:14 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n1", "n2", "n3" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:15 (Bool "for" (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:16 (Bool "for" (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:17 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: GENEALG1:18 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ))))) ; theorem :: GENEALG1:19 (Bool "for" (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" ))))) ; theorem :: GENEALG1:20 (Bool "for" (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ))))) ; theorem :: GENEALG1:21 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" ))))) ; theorem :: GENEALG1:22 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" ))))) ; theorem :: GENEALG1:23 (Bool "for" (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" ))))) ; theorem :: GENEALG1:24 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; theorem :: GENEALG1:25 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:26 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ))))) ; theorem :: GENEALG1:27 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" )) ")" )))) ; begin theorem :: GENEALG1:28 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n1", "n2", "n3", "n4" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:29 (Bool "for" (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" )))) ; theorem :: GENEALG1:30 (Bool "for" (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n2")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:31 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n4")) ")" )) ")" )))) ; theorem :: GENEALG1:32 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1"))))) ; theorem :: GENEALG1:33 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:34 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:35 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:36 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; theorem :: GENEALG1:37 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n3")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n3")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n2")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) ")" )) ")" )))) ; theorem :: GENEALG1:38 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:39 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n3")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n2")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) ")" )))) ; begin theorem :: GENEALG1:40 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n1", "n2", "n3", "n4", "n5" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:41 (Bool "for" (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" )))) ; theorem :: GENEALG1:42 (Bool "for" (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n2")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" )))) ; theorem :: GENEALG1:43 (Bool "for" (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" )))) ; theorem :: GENEALG1:44 (Bool "for" (Set (Var "n5")) "," (Set (Var "n4")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" )) ")" )))) ; theorem :: GENEALG1:45 (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: GENEALG1:46 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:47 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:48 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:49 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n5")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:50 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")))) & (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "holds" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "p1")))))) ; theorem :: GENEALG1:51 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n5")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) ")" )) ")" )))) ; theorem :: GENEALG1:52 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n5")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) ")" )) & (Bool (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) ")" )) ")" )))) ; begin theorem :: GENEALG1:53 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k6_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) "is" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")))))) ; definitionlet "S" be ($#m1_hidden :::"Gene-Set":::); let "p1", "p2" be ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Const "S")); let "n1", "n2", "n3", "n4", "n5", "n6" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"crossover"::: redefine func :::"crossover"::: "(" "p1" "," "p2" "," "n1" "," "n2" "," "n3" "," "n4" "," "n5" "," "n6" ")" -> ($#m1_genealg1 :::"Individual"::: ) "of" "S"; end; theorem :: GENEALG1:54 (Bool "for" (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "," (Set (Var "n1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p2")) "," (Set (Var "p1")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" )))) ; theorem :: GENEALG1:55 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n1")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n2")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n3")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n4")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n5")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n6")) ")" )) ")" & "(" (Bool (Bool (Set (Var "n6")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1"))))) "implies" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" ")" )))) ; theorem :: GENEALG1:56 (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n4")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n5")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n6")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n1")) ")" )) ")" )))) ; theorem :: GENEALG1:57 (Bool "for" (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) "," (Set (Var "n2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_hidden :::"Gene-Set":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_genealg1 :::"Individual"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n1")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n1")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n1")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n5")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n1")) "," (Set (Var "n6")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n6")) ")" )) & (Bool (Set ($#k12_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) "," (Set (Var "n1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_genealg1 :::"crossover"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "n2")) "," (Set (Var "n3")) "," (Set (Var "n4")) "," (Set (Var "n5")) ")" )) ")" )))) ;