genealg1.miz



    begin

    reserve D for non empty set;

    reserve f1,f2 for FinSequence of D;

    reserve i,n,n1,n2,n3,n4,n5,n6 for Element of NAT ;

    theorem :: GENEALG1:1

    

     Th1: for n be Nat holds n <= ( len f1) implies ((f1 ^ f2) /^ n) = ((f1 /^ n) ^ f2)

    proof

      let n be Nat;

      assume

       A1: n <= ( len f1);

      reconsider n as Element of NAT by ORDINAL1:def 12;

      ( len (f1 ^ f2)) = (( len f1) + ( len f2)) by FINSEQ_1: 22;

      then ( len f1) <= ( len (f1 ^ f2)) by NAT_1: 11;

      then

       A2: n <= ( len (f1 ^ f2)) by A1, XXREAL_0: 2;

      then

       A3: ( len ((f1 ^ f2) /^ n)) = (( len (f1 ^ f2)) - n) by RFINSEQ:def 1;

      

       A4: ( len ((f1 /^ n) ^ f2)) = (( len (f1 /^ n)) + ( len f2)) by FINSEQ_1: 22

      .= ((( len f1) - n) + ( len f2)) by A1, RFINSEQ:def 1

      .= ((( len f1) + ( len f2)) - n);

      

       A5: for i be Nat st 1 <= i & i <= ( len ((f1 ^ f2) /^ n)) holds (((f1 ^ f2) /^ n) . i) = (((f1 /^ n) ^ f2) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ((f1 ^ f2) /^ n));

        i in ( Seg ( len ((f1 ^ f2) /^ n))) by A6, A7, FINSEQ_1: 1;

        then

         A8: i in ( dom ((f1 ^ f2) /^ n)) by FINSEQ_1:def 3;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        now

          per cases ;

            suppose

             A9: i <= (( len f1) - n);

            i <= (i + n) by NAT_1: 11;

            then

             A10: 1 <= (i + n) by A6, XXREAL_0: 2;

            (i + n) <= ( len f1) by A9, XREAL_1: 19;

            then (i + n) in ( Seg ( len f1)) by A10, FINSEQ_1: 1;

            then

             A11: (i + n) in ( dom f1) by FINSEQ_1:def 3;

            i <= ( len (f1 /^ n)) by A1, A9, RFINSEQ:def 1;

            then i in ( Seg ( len (f1 /^ n))) by A6, FINSEQ_1: 1;

            then

             A12: i in ( dom (f1 /^ n)) by FINSEQ_1:def 3;

            

            then

             A13: (((f1 /^ n) ^ f2) . i) = ((f1 /^ n) . i) by FINSEQ_1:def 7

            .= (f1 . (i + n)) by A1, A12, RFINSEQ:def 1;

            (((f1 ^ f2) /^ n) . i) = ((f1 ^ f2) . (i + n)) by A2, A8, RFINSEQ:def 1

            .= (f1 . (i + n)) by A11, FINSEQ_1:def 7;

            hence thesis by A13;

          end;

            suppose

             A14: (( len f1) - n) < i;

            then

             A15: ( len (f1 /^ n)) < i by A1, RFINSEQ:def 1;

            i <= ( len ((f1 /^ n) ^ f2)) by A3, A4, A7, FINSEQ_1: 22;

            

            then

             A16: (((f1 /^ n) ^ f2) . i) = (f2 . (i - ( len (f1 /^ n)))) by A15, FINSEQ_1: 24

            .= (f2 . (i - (( len f1) - n))) by A1, RFINSEQ:def 1

            .= (f2 . ((i + n) - ( len f1)));

            

             A17: (i + n) <= ( len (f1 ^ f2)) by A3, A7, XREAL_1: 19;

            

             A18: ( len f1) < (i + n) by A14, XREAL_1: 19;

            (((f1 ^ f2) /^ n) . i) = ((f1 ^ f2) . (i + n)) by A2, A8, RFINSEQ:def 1

            .= (f2 . ((i + n) - ( len f1))) by A18, A17, FINSEQ_1: 24;

            hence thesis by A16;

          end;

        end;

        hence thesis;

      end;

      ( len ((f1 ^ f2) /^ n)) = ( len ((f1 /^ n) ^ f2)) by A3, A4, FINSEQ_1: 22;

      hence thesis by A5, FINSEQ_1: 14;

    end;

    theorem :: GENEALG1:2

    

     Th2: ((f1 ^ f2) | (( len f1) + i)) = (f1 ^ (f2 | i))

    proof

      ((f1 ^ f2) | (( len f1) + i)) = ((f1 ^ f2) | ( Seg (( len f1) + i))) & (f2 | i) = (f2 | ( Seg i)) by FINSEQ_1:def 15;

      hence thesis by FINSEQ_6: 14;

    end;

    definition

      mode Gene-Set is non-empty non empty FinSequence;

    end

    notation

      let S be Gene-Set;

      synonym GA-Space S for Union S;

    end

    registration

      let f be non-empty non empty Function;

      cluster ( Union f) -> non empty;

      coherence

      proof

        ( Union f) = ( union ( rng f)) by CARD_3:def 4;

        hence thesis;

      end;

    end

    definition

      let S be Gene-Set;

      :: GENEALG1:def1

      mode Individual of S -> FinSequence of ( GA-Space S) means

      : Def1: ( len it ) = ( len S) & for i st i in ( dom it ) holds (it . i) in (S . i);

      existence

      proof

        defpred P[ set, set] means $2 in (S . $1);

        

         A1: for k be Nat st k in ( Seg ( len S)) holds ex x be Element of ( GA-Space S) st P[k, x]

        proof

          let k be Nat;

          assume

           A2: k in ( Seg ( len S));

          then

          reconsider k9 = k as Element of ( dom S) by FINSEQ_1:def 3;

          (S . k9) <> {} ;

          then

          consider x be Element of (S . k) such that

           A3: x in ( [#] (S . k)) by SUBSET_1: 4;

          k in ( dom S) by A2, FINSEQ_1:def 3;

          then (S . k) in ( rng S) by FUNCT_1:def 3;

          then ( [#] (S . k)) c= ( union ( rng S)) by ZFMISC_1: 74;

          then

          reconsider x as Element of ( GA-Space S) by A3, CARD_3:def 4;

          take x;

          thus thesis by A3;

        end;

        consider IT be FinSequence of ( GA-Space S) such that

         A4: ( dom IT) = ( Seg ( len S)) & for k be Nat st k in ( Seg ( len S)) holds P[k, (IT . k)] from FINSEQ_1:sch 5( A1);

        take IT;

        thus thesis by A4, FINSEQ_1:def 3;

      end;

    end

    begin

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n;

      :: GENEALG1:def2

      func crossover (p1,p2,n) -> FinSequence of ( GA-Space S) equals ((p1 | n) ^ (p2 /^ n));

      correctness ;

    end

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n1, n2;

      :: GENEALG1:def3

      func crossover (p1,p2,n1,n2) -> FinSequence of ( GA-Space S) equals ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n2));

      correctness ;

    end

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n1, n2, n3;

      :: GENEALG1:def4

      func crossover (p1,p2,n1,n2,n3) -> FinSequence of ( GA-Space S) equals ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)),n3));

      correctness ;

    end

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n1, n2, n3, n4;

      :: GENEALG1:def5

      func crossover (p1,p2,n1,n2,n3,n4) -> FinSequence of ( GA-Space S) equals ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3)),n4));

      correctness ;

    end

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n1, n2, n3, n4, n5;

      :: GENEALG1:def6

      func crossover (p1,p2,n1,n2,n3,n4,n5) -> FinSequence of ( GA-Space S) equals ( crossover (( crossover (p1,p2,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5));

      correctness ;

    end

    definition

      let S be Gene-Set, p1,p2 be FinSequence of ( GA-Space S), n1, n2, n3, n4, n5, n6;

      :: GENEALG1:def7

      func crossover (p1,p2,n1,n2,n3,n4,n5,n6) -> FinSequence of ( GA-Space S) equals ( crossover (( crossover (p1,p2,n1,n2,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6));

      correctness ;

    end

    begin

    reserve S for Gene-Set;

    reserve p1,p2 for Individual of S;

    theorem :: GENEALG1:3

    

     Th3: ( crossover (p1,p2,n)) is Individual of S

    proof

      

       A1: ( len ( crossover (p1,p2,n))) = ( len S)

      proof

        

         A2: ( len ( crossover (p1,p2,n))) = (( len (p1 | n)) + ( len (p2 /^ n))) by FINSEQ_1: 22;

        now

          per cases ;

            suppose

             A3: n <= ( len p1);

            ( len (p2 /^ n)) = (( len p2) -' n) by RFINSEQ: 29

            .= (( len S) -' n) by Def1

            .= (( len p1) -' n) by Def1

            .= (( len p1) - n) by A3, XREAL_1: 233;

            

            then ( len ( crossover (p1,p2,n))) = (n + (( len p1) - n)) by A2, A3, FINSEQ_1: 59

            .= ( len p1);

            hence thesis by Def1;

          end;

            suppose

             A4: n > ( len p1);

            (p1 | n) = (p1 | ( Seg n)) by FINSEQ_1:def 15;

            then

             A5: (p1 | n) = p1 by A4, FINSEQ_2: 20;

            

             A6: (( len p1) - n) < 0 by A4, XREAL_1: 49;

            ( len (p2 /^ n)) = (( len p2) -' n) by RFINSEQ: 29

            .= (( len S) -' n) by Def1

            .= (( len p1) -' n) by Def1

            .= 0 by A6, XREAL_0:def 2;

            hence thesis by A2, A5, Def1;

          end;

        end;

        hence thesis;

      end;

      for i st i in ( dom ( crossover (p1,p2,n))) holds (( crossover (p1,p2,n)) . i) in (S . i)

      proof

        let i;

        assume

         A7: i in ( dom ( crossover (p1,p2,n)));

        now

          per cases by A7, FINSEQ_1: 25;

            suppose

             A8: i in ( dom (p1 | n));

            

             A9: ( dom (p1 | n)) c= ( dom p1) by FINSEQ_5: 18;

            ((p1 | n) . i) = ((p1 | n) /. i) by A8, PARTFUN1:def 6

            .= (p1 /. i) by A8, FINSEQ_4: 70

            .= (p1 . i) by A8, A9, PARTFUN1:def 6;

            then ((p1 | n) . i) in (S . i) by A8, A9, Def1;

            hence thesis by A8, FINSEQ_1:def 7;

          end;

            suppose ex k be Nat st k in ( dom (p2 /^ n)) & i = (( len (p1 | n)) + k);

            then

            consider k be Nat such that

             A10: k in ( dom (p2 /^ n)) and

             A11: i = (( len (p1 | n)) + k);

            reconsider k as Element of NAT by ORDINAL1:def 12;

            

             A12: n <= ( len (p1 | n))

            proof

              (n + k) in ( dom p2) by A10, FINSEQ_5: 26;

              then (n + k) in ( Seg ( len p2)) by FINSEQ_1:def 3;

              then (n + k) <= ( len p2) by FINSEQ_1: 1;

              then (n + k) <= ( len S) by Def1;

              then (n + k) <= ( len p1) by Def1;

              then

               A13: k <= (( len p1) - n) by XREAL_1: 19;

              k in ( Seg ( len (p2 /^ n))) by A10, FINSEQ_1:def 3;

              then 1 <= k by FINSEQ_1: 1;

              then 1 <= (( len p1) - n) by A13, XXREAL_0: 2;

              then (1 + n) <= ( len p1) by XREAL_1: 19;

              then

               A14: n <= (( len p1) - 1) by XREAL_1: 19;

              ( len p1) <= (( len p1) + 1) by NAT_1: 11;

              then

               A15: (( len p1) - 1) <= ( len p1) by XREAL_1: 20;

              assume n > ( len (p1 | n));

              hence contradiction by A14, A15, FINSEQ_1: 59, XXREAL_0: 2;

            end;

            ( len (p1 | n)) <= n by FINSEQ_5: 17;

            then

             A16: ( len (p1 | n)) = n by A12, XXREAL_0: 1;

            then (n + k) in ( Seg ( len S)) by A1, A7, A11, FINSEQ_1:def 3;

            then (n + k) in ( Seg ( len p2)) by Def1;

            then

             A17: (n + k) in ( dom p2) by FINSEQ_1:def 3;

            (( crossover (p1,p2,n)) . i) = ((p2 /^ n) . k) by A10, A11, FINSEQ_1:def 7

            .= ((p2 /^ n) /. k) by A10, PARTFUN1:def 6

            .= (p2 /. (n + k)) by A10, FINSEQ_5: 27

            .= (p2 . (n + k)) by A17, PARTFUN1:def 6;

            hence thesis by A11, A16, A17, Def1;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, Def1;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n;

      :: original: crossover

      redefine

      func crossover (p1,p2,n) -> Individual of S ;

      correctness by Th3;

    end

    theorem :: GENEALG1:4

    

     Th4: ( crossover (p1,p2, 0 )) = p2

    proof

      ( crossover (p1,p2, 0 )) = (p2 /^ 0 ) by FINSEQ_1: 34

      .= p2 by FINSEQ_5: 28;

      hence thesis;

    end;

    theorem :: GENEALG1:5

    

     Th5: n >= ( len p1) implies ( crossover (p1,p2,n)) = p1

    proof

      assume

       A1: n >= ( len p1);

      then n >= ( len S) by Def1;

      then

       A2: n >= ( len p2) by Def1;

      ( crossover (p1,p2,n)) = (p1 ^ (p2 /^ n)) by A1, FINSEQ_1: 58

      .= (p1 ^ {} ) by A2, FINSEQ_5: 32

      .= p1 by FINSEQ_1: 34;

      hence thesis;

    end;

    begin

    theorem :: GENEALG1:6

    

     Th6: ( crossover (p1,p2,n1,n2)) is Individual of S

    proof

      reconsider q1 = ( crossover (p1,p2,n1)), q2 = ( crossover (p2,p1,n1)) as Individual of S;

      ( crossover (q1,q2,n2)) is Individual of S;

      hence thesis;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n1, n2;

      :: original: crossover

      redefine

      func crossover (p1,p2,n1,n2) -> Individual of S ;

      correctness by Th6;

    end

    theorem :: GENEALG1:7

    

     Th7: ( crossover (p1,p2, 0 ,n)) = ( crossover (p2,p1,n))

    proof

      ( crossover (p1,p2, 0 ,n)) = ( crossover (p2,( crossover (p2,p1, 0 )),n)) by Th4

      .= ( crossover (p2,p1,n)) by Th4;

      hence thesis;

    end;

    theorem :: GENEALG1:8

    

     Th8: ( crossover (p1,p2,n, 0 )) = ( crossover (p2,p1,n))

    proof

      reconsider q1 = ( crossover (p1,p2,n)) as Individual of S;

      reconsider q2 = ( crossover (p2,p1,n)) as Individual of S;

      ( crossover (p1,p2,n, 0 )) = ( crossover (q1,q2, 0 ))

      .= q2 by Th4;

      hence thesis;

    end;

    theorem :: GENEALG1:9

    

     Th9: n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2)) = ( crossover (p1,p2,n2))

    proof

      assume

       A1: n1 >= ( len p1);

      then n1 >= ( len S) by Def1;

      then

       A2: n1 >= ( len p2) by Def1;

      ( crossover (p1,p2,n1,n2)) = ( crossover (p1,( crossover (p2,p1,n1)),n2)) by A1, Th5;

      hence thesis by A2, Th5;

    end;

    theorem :: GENEALG1:10

    

     Th10: n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2)) = ( crossover (p1,p2,n1))

    proof

      assume n2 >= ( len p1);

      then n2 >= ( len S) by Def1;

      then

       A1: n2 >= ( len ( crossover (p1,p2,n1))) by Def1;

      ( crossover (p1,p2,n1,n2)) = ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n2));

      hence thesis by A1, Th5;

    end;

    theorem :: GENEALG1:11

    n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2)) = p1

    proof

      assume that

       A1: n1 >= ( len p1) and

       A2: n2 >= ( len p1);

      ( crossover (p1,p2,n1,n2)) = ( crossover (p1,p2,n2)) by A1, Th9;

      hence thesis by A2, Th5;

    end;

    theorem :: GENEALG1:12

    

     Th12: ( crossover (p1,p2,n1,n1)) = p1

    proof

      

       A1: (((p2 | n1) ^ (p1 /^ n1)) /^ n1) = (p1 /^ n1)

      proof

        now

          per cases ;

            suppose n1 <= ( len p2);

            then ( len (p2 | n1)) = n1 by FINSEQ_1: 59;

            hence thesis by FINSEQ_5: 37;

          end;

            suppose n1 > ( len p2);

            then

             A2: n1 > ( len S) by Def1;

            then n1 > ( len ( crossover (p2,p1,n1))) by Def1;

            then

             A3: (((p2 | n1) ^ (p1 /^ n1)) /^ n1) = {} by FINSEQ_5: 32;

            n1 > ( len p1) by A2, Def1;

            hence thesis by A3, FINSEQ_5: 32;

          end;

        end;

        hence thesis;

      end;

      (((p1 | n1) ^ (p2 /^ n1)) | n1) = (p1 | n1)

      proof

        now

          per cases ;

            suppose n1 <= ( len p1);

            then ( len (p1 | n1)) = n1 by FINSEQ_1: 59;

            hence thesis by FINSEQ_5: 23;

          end;

            suppose

             A4: n1 > ( len p1);

            then

             A5: n1 > ( len S) by Def1;

            then

             A6: n1 > ( len p2) by Def1;

            n1 > ( len ( crossover (p1,p2,n1))) by A5, Def1;

            

            then (((p1 | n1) ^ (p2 /^ n1)) | n1) = ((p1 | n1) ^ (p2 /^ n1)) by FINSEQ_1: 58

            .= (p1 ^ (p2 /^ n1)) by A4, FINSEQ_1: 58

            .= (p1 ^ {} ) by A6, FINSEQ_5: 32

            .= p1 by FINSEQ_1: 34

            .= (p1 | n1) by A4, FINSEQ_1: 58;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, RFINSEQ: 8;

    end;

    theorem :: GENEALG1:13

    

     Th13: ( crossover (p1,p2,n1,n2)) = ( crossover (p1,p2,n2,n1))

    proof

      

       A1: ( len p1) = ( len S) by Def1;

      ( len ((p2 | n2) ^ (p1 /^ n2))) = ( len ( crossover (p2,p1,n2)));

      then

       A2: ( len ((p2 | n2) ^ (p1 /^ n2))) = ( len S) by Def1;

      

       A3: ( len p2) = ( len S) by Def1;

      ( len ((p1 | n2) ^ (p2 /^ n2))) = ( len ( crossover (p1,p2,n2)));

      then

       A4: ( len ((p1 | n2) ^ (p2 /^ n2))) = ( len S) by Def1;

      now

        per cases by NAT_1: 3;

          suppose

           A5: n1 >= n2 & n2 > 0 ;

          now

            per cases ;

              suppose

               A6: n1 >= ( len p1);

              then (p2 | n1) = p2 by A1, A3, FINSEQ_1: 58;

              

              then

               A7: ((p2 | n1) ^ (p1 /^ n1)) = (p2 ^ {} ) by A6, FINSEQ_5: 32

              .= p2 by FINSEQ_1: 34;

              (p1 | n1) = p1 by A6, FINSEQ_1: 58;

              

              then

               A8: ((p1 | n1) ^ (p2 /^ n1)) = (p1 ^ {} ) by A1, A3, A6, FINSEQ_5: 32

              .= p1 by FINSEQ_1: 34;

              (((p1 | n2) ^ (p2 /^ n2)) | n1) = ((p1 | n2) ^ (p2 /^ n2)) by A1, A4, A6, FINSEQ_1: 58;

              

              then ( crossover (p1,p2,n2,n1)) = (((p1 | n2) ^ (p2 /^ n2)) ^ {} ) by A1, A2, A6, FINSEQ_5: 32

              .= ((p1 | n2) ^ (p2 /^ n2)) by FINSEQ_1: 34;

              hence thesis by A8, A7;

            end;

              suppose

               A9: n1 < ( len p1);

              then ( len (p1 | n1)) = n1 by FINSEQ_1: 59;

              

              then

               A10: (((p1 | n1) ^ (p2 /^ n1)) | n2) = ((p1 | n1) | n2) by A5, FINSEQ_5: 22

              .= (p1 | n2) by A5, FINSEQ_5: 77;

              n1 <= ( len p2) by A3, A9, Def1;

              then n2 <= ( len (p2 | n1)) by A5, FINSEQ_1: 59;

              

              then

               A11: ( crossover (p1,p2,n1,n2)) = ((p1 | n2) ^ (((p2 | n1) /^ n2) ^ (p1 /^ n1))) by A10, Th1

              .= (((p1 | n2) ^ ((p2 | n1) /^ n2)) ^ (p1 /^ n1)) by FINSEQ_1: 32;

              ( len (p2 | n2)) = n2 by A1, A3, A5, A9, FINSEQ_1: 59, XXREAL_0: 2;

              then

              consider i be Nat such that

               A12: (( len (p2 | n2)) + i) = n1 by A5, NAT_1: 10;

              reconsider i as Element of NAT by ORDINAL1:def 12;

              

               A13: ( len (p1 | n2)) = n2 by A5, A9, FINSEQ_1: 59, XXREAL_0: 2;

              then

               A14: (( len (p1 | n2)) + i) = n1 by A1, A3, A5, A9, A12, FINSEQ_1: 59, XXREAL_0: 2;

              then i = (n1 - n2) by A13;

              then

               A15: i = (n1 -' n2) by A5, XREAL_1: 233;

              

               A16: (((p1 | n2) ^ (p2 /^ n2)) | n1) = ((p1 | n2) ^ ((p2 /^ n2) | i)) by A14, Th2

              .= ((p1 | n2) ^ ((p2 | n1) /^ n2)) by A15, FINSEQ_5: 80;

              (((p2 | n2) ^ (p1 /^ n2)) /^ n1) = ((p1 /^ n2) /^ i) by A12, FINSEQ_5: 36

              .= (p1 /^ (n2 + i)) by FINSEQ_6: 81

              .= (p1 /^ n1) by A1, A3, A5, A9, A12, FINSEQ_1: 59, XXREAL_0: 2;

              hence thesis by A11, A16;

            end;

          end;

          hence thesis;

        end;

          suppose

           A17: n1 < n2 & n2 > 0 ;

          now

            per cases ;

              suppose

               A18: n1 >= ( len p1);

              then n2 >= ( len p1) by A17, XXREAL_0: 2;

              then

               A19: n2 >= ( len p2) by A3, Def1;

              

               A20: n1 >= ( len p2) by A3, A18, Def1;

              then (p2 | n1) = p2 by FINSEQ_1: 58;

              

              then ((p2 | n1) ^ (p1 /^ n1)) = (p2 ^ {} ) by A18, FINSEQ_5: 32

              .= p2 by FINSEQ_1: 34;

              then

               A21: (((p2 | n1) ^ (p1 /^ n1)) /^ n2) = {} by A19, FINSEQ_5: 32;

              (p1 | n2) = p1 by A17, A18, FINSEQ_1: 58, XXREAL_0: 2;

              

              then ((p1 | n2) ^ (p2 /^ n2)) = (p1 ^ {} ) by A19, FINSEQ_5: 32

              .= p1 by FINSEQ_1: 34;

              then

               A22: (((p1 | n2) ^ (p2 /^ n2)) | n1) = p1 by A18, FINSEQ_1: 58;

              (p2 | n2) = p2 by A19, FINSEQ_1: 58;

              

              then ((p2 | n2) ^ (p1 /^ n2)) = (p2 ^ {} ) by A17, A18, FINSEQ_5: 32, XXREAL_0: 2

              .= p2 by FINSEQ_1: 34;

              then

               A23: (((p2 | n2) ^ (p1 /^ n2)) /^ n1) = {} by A20, FINSEQ_5: 32;

              (p1 | n1) = p1 by A18, FINSEQ_1: 58;

              

              then ((p1 | n1) ^ (p2 /^ n1)) = (p1 ^ {} ) by A20, FINSEQ_5: 32

              .= p1 by FINSEQ_1: 34;

              hence thesis by A17, A18, A21, A22, A23, FINSEQ_1: 58, XXREAL_0: 2;

            end;

              suppose

               A24: n1 < ( len p1);

              n1 <= ( len (p1 | n2))

              proof

                now

                  per cases ;

                    suppose n2 >= ( len p1);

                    hence thesis by A24, FINSEQ_1: 58;

                  end;

                    suppose n2 < ( len p1);

                    hence thesis by A17, FINSEQ_1: 59;

                  end;

                end;

                hence thesis;

              end;

              

              then

               A25: (((p1 | n2) ^ (p2 /^ n2)) | n1) = ((p1 | n2) | n1) by FINSEQ_5: 22

              .= (p1 | n1) by A17, FINSEQ_5: 77;

              

               A26: ( len (p1 | n1)) = n1 by A24, FINSEQ_1: 59;

              then

              consider i be Nat such that

               A27: (( len (p1 | n1)) + i) = n2 by A17, NAT_1: 10;

              reconsider i as Element of NAT by ORDINAL1:def 12;

              

               A28: (((p1 | n1) ^ (p2 /^ n1)) | n2) = ((p1 | n1) ^ ((p2 /^ n1) | i)) by A27, Th2;

              ( len (p2 | n1)) = n1 by A1, A3, A24, FINSEQ_1: 59;

              then (( len (p2 | n1)) + i) = n2 by A24, A27, FINSEQ_1: 59;

              

              then

               A29: ( crossover (p1,p2,n1,n2)) = (((p1 | n1) ^ ((p2 /^ n1) | i)) ^ ((p1 /^ n1) /^ i)) by A28, FINSEQ_5: 36

              .= (((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ (n1 + i))) by FINSEQ_6: 81

              .= (((p1 | n1) ^ ((p2 /^ n1) | i)) ^ (p1 /^ n2)) by A24, A27, FINSEQ_1: 59;

              

               A30: i = (n2 - n1) by A26, A27;

              n1 <= ( len (p2 | n2))

              proof

                now

                  per cases ;

                    suppose n2 >= ( len p2);

                    hence thesis by A1, A3, A24, FINSEQ_1: 58;

                  end;

                    suppose n2 < ( len p2);

                    hence thesis by A17, FINSEQ_1: 59;

                  end;

                end;

                hence thesis;

              end;

              

              then (((p2 | n2) ^ (p1 /^ n2)) /^ n1) = (((p2 | n2) /^ n1) ^ (p1 /^ n2)) by Th1

              .= (((p2 /^ n1) | (n2 -' n1)) ^ (p1 /^ n2)) by FINSEQ_5: 80

              .= (((p2 /^ n1) | i) ^ (p1 /^ n2)) by A17, A30, XREAL_1: 233;

              hence thesis by A29, A25, FINSEQ_1: 32;

            end;

          end;

          hence thesis;

        end;

          suppose

           A31: n2 = 0 ;

          

          then ( crossover (p1,p2,n1,n2)) = ( crossover (p2,p1,n1)) by Th8

          .= ( crossover (p1,p2, 0 ,n1)) by Th7;

          hence thesis by A31;

        end;

      end;

      hence thesis;

    end;

    begin

    theorem :: GENEALG1:14

    

     Th14: ( crossover (p1,p2,n1,n2,n3)) is Individual of S

    proof

      reconsider q1 = ( crossover (p1,p2,n1,n2)), q2 = ( crossover (p2,p1,n1,n2)) as Individual of S;

      ( crossover (q1,q2,n3)) is Individual of S;

      hence thesis;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n1, n2, n3;

      :: original: crossover

      redefine

      func crossover (p1,p2,n1,n2,n3) -> Individual of S ;

      correctness by Th14;

    end

    theorem :: GENEALG1:15

    

     Th15: ( crossover (p1,p2, 0 ,n2,n3)) = ( crossover (p2,p1,n2,n3)) & ( crossover (p1,p2,n1, 0 ,n3)) = ( crossover (p2,p1,n1,n3)) & ( crossover (p1,p2,n1,n2, 0 )) = ( crossover (p2,p1,n1,n2))

    proof

      ( crossover (p1,p2, 0 ,n2,n3)) = ( crossover (( crossover (p2,p1,n2)),( crossover (p2,p1, 0 ,n2)),n3)) by Th7

      .= ( crossover (( crossover (p2,p1,n2)),( crossover (p1,p2,n2)),n3)) by Th7;

      hence ( crossover (p1,p2, 0 ,n2,n3)) = ( crossover (p2,p1,n2,n3));

      ( crossover (p1,p2,n1, 0 ,n3)) = ( crossover (( crossover (p2,p1,n1)),( crossover (p2,p1,n1, 0 )),n3)) by Th8

      .= ( crossover (( crossover (p2,p1,n1)),( crossover (p1,p2,n1)),n3)) by Th8;

      hence ( crossover (p1,p2,n1, 0 ,n3)) = ( crossover (p2,p1,n1,n3));

      ( crossover (p1,p2,n1,n2, 0 )) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)), 0 ));

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:16

    ( crossover (p1,p2, 0 , 0 ,n3)) = ( crossover (p1,p2,n3)) & ( crossover (p1,p2,n1, 0 , 0 )) = ( crossover (p1,p2,n1)) & ( crossover (p1,p2, 0 ,n2, 0 )) = ( crossover (p1,p2,n2))

    proof

      ( crossover (p1,p2, 0 , 0 ,n3)) = ( crossover (p1,( crossover (p2,p1, 0 , 0 )),n3)) by Th12;

      hence ( crossover (p1,p2, 0 , 0 ,n3)) = ( crossover (p1,p2,n3)) by Th12;

      ( crossover (p1,p2,n1, 0 , 0 )) = ( crossover (( crossover (p2,p1,n1)),( crossover (p1,p2,n1)), 0 )) by Th8;

      hence ( crossover (p1,p2,n1, 0 , 0 )) = ( crossover (p1,p2,n1)) by Th4;

      ( crossover (p1,p2, 0 ,n2, 0 )) = ( crossover (( crossover (p2,p1,n2)),( crossover (p1,p2,n2)), 0 )) by Th7;

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:17

    ( crossover (p1,p2, 0 , 0 , 0 )) = p2

    proof

      ( crossover (p1,p2, 0 , 0 , 0 )) = ( crossover (( crossover (p1,p2, 0 , 0 )),p2, 0 )) by Th12;

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:18

    

     Th18: n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2,n3))

    proof

      assume

       A1: n1 >= ( len p1);

      then n1 >= ( len S) by Def1;

      then

       A2: n1 >= ( len p2) by Def1;

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n1,n2)),n3)) by A1, Th9

      .= ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n2)),n3)) by A2, Th9;

      hence thesis;

    end;

    theorem :: GENEALG1:19

    

     Th19: n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1,n3))

    proof

      assume

       A1: n2 >= ( len p1);

      then n2 >= ( len S) by Def1;

      then

       A2: n2 >= ( len p2) by Def1;

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n2)),n3)) by A1, Th10

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n3)) by A2, Th10;

      hence thesis;

    end;

    theorem :: GENEALG1:20

    

     Th20: n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1,n2))

    proof

      assume n3 >= ( len p1);

      then n3 >= ( len S) by Def1;

      then

       A1: n3 >= ( len ( crossover (p1,p2,n1,n2))) by Def1;

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)),n3));

      hence thesis by A1, Th5;

    end;

    theorem :: GENEALG1:21

    

     Th21: n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n3))

    proof

      assume that

       A1: n1 >= ( len p1) and

       A2: n2 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2,n3)) by A1, Th18;

      hence thesis by A2, Th9;

    end;

    theorem :: GENEALG1:22

    n1 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2))

    proof

      assume that

       A1: n1 >= ( len p1) and

       A2: n3 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2,n3)) by A1, Th18;

      hence thesis by A2, Th10;

    end;

    theorem :: GENEALG1:23

    n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1))

    proof

      assume that

       A1: n2 >= ( len p1) and

       A2: n3 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1,n3)) by A1, Th19;

      hence thesis by A2, Th10;

    end;

    theorem :: GENEALG1:24

    n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3)) = p1

    proof

      assume that

       A1: n1 >= ( len p1) & n2 >= ( len p1) and

       A2: n3 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n3)) by A1, Th21;

      hence thesis by A2, Th5;

    end;

    theorem :: GENEALG1:25

    

     Th25: ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2,n1,n3)) & ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1,n3,n2))

    proof

      set q1 = ( crossover (p1,p2,n1));

      set q2 = ( crossover (p2,p1,n1));

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (( crossover (p1,p2,n2,n1)),( crossover (p2,p1,n1,n2)),n3)) by Th13

      .= ( crossover (( crossover (p1,p2,n2,n1)),( crossover (p2,p1,n2,n1)),n3)) by Th13;

      hence ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n2,n1,n3));

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (q1,q2,n2,n3))

      .= ( crossover (q1,q2,n3,n2)) by Th13

      .= ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n3)),n2));

      hence thesis;

    end;

    theorem :: GENEALG1:26

    

     Th26: ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n3,n1,n2))

    proof

      ( crossover (p1,p2,n1,n2,n3)) = ( crossover (p1,p2,n1,n3,n2)) by Th25;

      hence thesis by Th25;

    end;

    theorem :: GENEALG1:27

    

     Th27: ( crossover (p1,p2,n1,n1,n3)) = ( crossover (p1,p2,n3)) & ( crossover (p1,p2,n1,n2,n1)) = ( crossover (p1,p2,n2)) & ( crossover (p1,p2,n1,n2,n2)) = ( crossover (p1,p2,n1))

    proof

      ( crossover (p1,p2,n1,n1,n3)) = ( crossover (p1,( crossover (p2,p1,n1,n1)),n3)) by Th12;

      hence ( crossover (p1,p2,n1,n1,n3)) = ( crossover (p1,p2,n3)) by Th12;

      ( crossover (p1,p2,n1,n2,n1)) = ( crossover (p1,p2,n1,n1,n2)) by Th25

      .= ( crossover (p1,( crossover (p2,p1,n1,n1)),n2)) by Th12;

      hence ( crossover (p1,p2,n1,n2,n1)) = ( crossover (p1,p2,n2)) by Th12;

      

      thus ( crossover (p1,p2,n1,n2,n2)) = ( crossover (p1,p2,n2,n2,n1)) by Th26

      .= ( crossover (p1,( crossover (p2,p1,n2,n2)),n1)) by Th12

      .= ( crossover (p1,p2,n1)) by Th12;

    end;

    begin

    theorem :: GENEALG1:28

    

     Th28: ( crossover (p1,p2,n1,n2,n3,n4)) is Individual of S

    proof

      reconsider q1 = ( crossover (p1,p2,n1,n2,n3)), q2 = ( crossover (p2,p1,n1,n2,n3)) as Individual of S;

      ( crossover (q1,q2,n4)) is Individual of S;

      hence thesis;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n1, n2, n3, n4;

      :: original: crossover

      redefine

      func crossover (p1,p2,n1,n2,n3,n4) -> Individual of S ;

      correctness by Th28;

    end

    theorem :: GENEALG1:29

    

     Th29: ( crossover (p1,p2, 0 ,n2,n3,n4)) = ( crossover (p2,p1,n2,n3,n4)) & ( crossover (p1,p2,n1, 0 ,n3,n4)) = ( crossover (p2,p1,n1,n3,n4)) & ( crossover (p1,p2,n1,n2, 0 ,n4)) = ( crossover (p2,p1,n1,n2,n4)) & ( crossover (p1,p2,n1,n2,n3, 0 )) = ( crossover (p2,p1,n1,n2,n3))

    proof

      ( crossover (p1,p2, 0 ,n2,n3,n4)) = ( crossover (( crossover (p2,p1,n2,n3)),( crossover (p2,p1, 0 ,n2,n3)),n4)) by Th15

      .= ( crossover (( crossover (p2,p1,n2,n3)),( crossover (p1,p2,n2,n3)),n4)) by Th15;

      hence ( crossover (p1,p2, 0 ,n2,n3,n4)) = ( crossover (p2,p1,n2,n3,n4));

      ( crossover (p1,p2,n1, 0 ,n3,n4)) = ( crossover (( crossover (p2,p1,n1,n3)),( crossover (p2,p1,n1, 0 ,n3)),n4)) by Th15

      .= ( crossover (( crossover (p2,p1,n1,n3)),( crossover (p1,p2,n1,n3)),n4)) by Th15;

      hence ( crossover (p1,p2,n1, 0 ,n3,n4)) = ( crossover (p2,p1,n1,n3,n4));

      ( crossover (p1,p2,n1,n2, 0 ,n4)) = ( crossover (( crossover (p2,p1,n1,n2)),( crossover (p2,p1,n1,n2, 0 )),n4)) by Th15

      .= ( crossover (( crossover (p2,p1,n1,n2)),( crossover (p1,p2,n1,n2)),n4)) by Th15;

      hence ( crossover (p1,p2,n1,n2, 0 ,n4)) = ( crossover (p2,p1,n1,n2,n4));

      ( crossover (p1,p2,n1,n2,n3, 0 )) = ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3)), 0 ));

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:30

    

     Th30: ( crossover (p1,p2, 0 , 0 ,n3,n4)) = ( crossover (p1,p2,n3,n4)) & ( crossover (p1,p2, 0 ,n2, 0 ,n4)) = ( crossover (p1,p2,n2,n4)) & ( crossover (p1,p2, 0 ,n2,n3, 0 )) = ( crossover (p1,p2,n2,n3)) & ( crossover (p1,p2,n1, 0 ,n3, 0 )) = ( crossover (p1,p2,n1,n3)) & ( crossover (p1,p2,n1, 0 , 0 ,n4)) = ( crossover (p1,p2,n1,n4)) & ( crossover (p1,p2,n1,n2, 0 , 0 )) = ( crossover (p1,p2,n1,n2))

    proof

      ( crossover (p1,p2, 0 , 0 ,n3,n4)) = ( crossover (p2,p1, 0 ,n3,n4)) by Th29;

      hence ( crossover (p1,p2, 0 , 0 ,n3,n4)) = ( crossover (p1,p2,n3,n4)) by Th15;

      ( crossover (p1,p2, 0 ,n2, 0 ,n4)) = ( crossover (p2,p1,n2, 0 ,n4)) by Th29;

      hence ( crossover (p1,p2, 0 ,n2, 0 ,n4)) = ( crossover (p1,p2,n2,n4)) by Th15;

      ( crossover (p1,p2, 0 ,n2,n3, 0 )) = ( crossover (p2,p1,n2,n3, 0 )) by Th29;

      hence ( crossover (p1,p2, 0 ,n2,n3, 0 )) = ( crossover (p1,p2,n2,n3)) by Th15;

      ( crossover (p1,p2,n1, 0 ,n3, 0 )) = ( crossover (p2,p1,n1,n3, 0 )) by Th29;

      hence ( crossover (p1,p2,n1, 0 ,n3, 0 )) = ( crossover (p1,p2,n1,n3)) by Th15;

      ( crossover (p1,p2,n1, 0 , 0 ,n4)) = ( crossover (p2,p1,n1, 0 ,n4)) by Th29;

      hence ( crossover (p1,p2,n1, 0 , 0 ,n4)) = ( crossover (p1,p2,n1,n4)) by Th15;

      ( crossover (p1,p2,n1,n2, 0 , 0 )) = ( crossover (p2,p1,n1,n2, 0 )) by Th29;

      hence thesis by Th15;

    end;

    theorem :: GENEALG1:31

    

     Th31: ( crossover (p1,p2,n1, 0 , 0 , 0 )) = ( crossover (p2,p1,n1)) & ( crossover (p1,p2, 0 ,n2, 0 , 0 )) = ( crossover (p2,p1,n2)) & ( crossover (p1,p2, 0 , 0 ,n3, 0 )) = ( crossover (p2,p1,n3)) & ( crossover (p1,p2, 0 , 0 , 0 ,n4)) = ( crossover (p2,p1,n4))

    proof

      ( crossover (p1,p2,n1, 0 , 0 , 0 )) = ( crossover (p1,p2,n1, 0 )) by Th30;

      hence ( crossover (p1,p2,n1, 0 , 0 , 0 )) = ( crossover (p2,p1,n1)) by Th8;

      ( crossover (p1,p2, 0 ,n2, 0 , 0 )) = ( crossover (p1,p2, 0 ,n2)) by Th30;

      hence ( crossover (p1,p2, 0 ,n2, 0 , 0 )) = ( crossover (p2,p1,n2)) by Th7;

      ( crossover (p1,p2, 0 , 0 ,n3, 0 )) = ( crossover (p1,p2, 0 ,n3)) by Th30;

      hence ( crossover (p1,p2, 0 , 0 ,n3, 0 )) = ( crossover (p2,p1,n3)) by Th7;

      ( crossover (p1,p2, 0 , 0 , 0 ,n4)) = ( crossover (p1,p2, 0 ,n4)) by Th30;

      hence thesis by Th7;

    end;

    theorem :: GENEALG1:32

    

     Th32: ( crossover (p1,p2, 0 , 0 , 0 , 0 )) = p1

    proof

      ( crossover (p1,p2, 0 , 0 , 0 , 0 )) = ( crossover (p2,p1, 0 )) by Th31;

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:33

    

     Th33: (n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4))) & (n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4))) & (n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n4))) & (n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n3)))

    proof

      

       A1: n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n3))

      proof

        assume n4 >= ( len p1);

        then n4 >= ( len S) by Def1;

        then

         A2: n4 >= ( len ( crossover (p1,p2,n1,n2,n3))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3)),n4));

        hence thesis by A2, Th5;

      end;

      

       A3: n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4))

      proof

        assume

         A4: n2 >= ( len p1);

        then n2 >= ( len S) by Def1;

        then

         A5: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by A4, Th19

        .= ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n3)),n4)) by A5, Th19;

        hence thesis;

      end;

      

       A6: n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n4))

      proof

        assume

         A7: n3 >= ( len p1);

        then n3 >= ( len S) by Def1;

        then

         A8: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by A7, Th20

        .= ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)),n4)) by A8, Th20;

        hence thesis;

      end;

      n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4))

      proof

        assume

         A9: n1 >= ( len p1);

        then n1 >= ( len S) by Def1;

        then

         A10: n1 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by A9, Th18

        .= ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n2,n3)),n4)) by A10, Th18;

        hence thesis;

      end;

      hence thesis by A3, A6, A1;

    end;

    theorem :: GENEALG1:34

    

     Th34: (n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4))) & (n1 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4))) & (n1 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3))) & (n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n4))) & (n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3))) & (n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2)))

    proof

      

       A1: n1 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4))

      proof

        assume that

         A2: n1 >= ( len p1) and

         A3: n3 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4)) by A2, Th33;

        hence thesis by A3, Th19;

      end;

      

       A4: n1 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3))

      proof

        assume that

         A5: n1 >= ( len p1) and

         A6: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4)) by A5, Th33;

        hence thesis by A6, Th20;

      end;

      

       A7: n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2))

      proof

        assume that

         A8: n3 >= ( len p1) and

         A9: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n4)) by A8, Th33;

        hence thesis by A9, Th20;

      end;

      

       A10: n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3))

      proof

        assume that

         A11: n2 >= ( len p1) and

         A12: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4)) by A11, Th33;

        hence thesis by A12, Th20;

      end;

      

       A13: n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n4))

      proof

        assume that

         A14: n2 >= ( len p1) and

         A15: n3 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4)) by A14, Th33;

        hence thesis by A15, Th19;

      end;

      n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4))

      proof

        assume that

         A16: n1 >= ( len p1) and

         A17: n2 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4)) by A16, Th33;

        hence thesis by A17, Th18;

      end;

      hence thesis by A1, A4, A13, A10, A7;

    end;

    theorem :: GENEALG1:35

    

     Th35: (n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4))) & (n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3))) & (n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2))) & (n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1)))

    proof

      

       A1: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4))

      proof

        assume that

         A2: n1 >= ( len p1) & n2 >= ( len p1) and

         A3: n3 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4)) by A2, Th34;

        hence thesis by A3, Th9;

      end;

      

       A4: n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2))

      proof

        assume that

         A5: n1 >= ( len p1) & n3 >= ( len p1) and

         A6: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4)) by A5, Th34

        .= ( crossover (p1,p2,n4,n2)) by Th13;

        hence thesis by A6, Th9;

      end;

      

       A7: n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1))

      proof

        assume that

         A8: n2 >= ( len p1) & n3 >= ( len p1) and

         A9: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n4)) by A8, Th34

        .= ( crossover (p1,p2,n4,n1)) by Th13;

        hence thesis by A9, Th9;

      end;

      n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3))

      proof

        assume that

         A10: n1 >= ( len p1) & n2 >= ( len p1) and

         A11: n4 >= ( len p1);

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4)) by A10, Th34

        .= ( crossover (p1,p2,n4,n3)) by Th13;

        hence thesis by A11, Th9;

      end;

      hence thesis by A1, A4, A7;

    end;

    theorem :: GENEALG1:36

    

     Th36: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4)) = p1

    proof

      assume that

       A1: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) and

       A2: n4 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4)) by A1, Th35;

      hence thesis by A2, Th5;

    end;

    theorem :: GENEALG1:37

    

     Th37: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n4,n3)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n2,n4)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4,n2)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n4,n3,n2)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n1,n3,n4)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n1,n4,n3)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n1,n4)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4,n1)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4,n1,n3)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4,n3,n1)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n2,n1,n4)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n2,n4,n1)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4,n1,n2)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4,n2,n1)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4,n2,n3,n1)) & ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4,n3,n2,n1))

    proof

      

       A1: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n2,n4,n3))

      proof

        set q2 = ( crossover (p2,p1,n1,n2));

        set q1 = ( crossover (p1,p2,n1,n2));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (q1,q2,n3,n4))

        .= ( crossover (q1,q2,n4,n3)) by Th13

        .= ( crossover (( crossover (q1,q2,n4)),( crossover (q2,q1,n4)),n3));

        hence thesis;

      end;

      

       A2: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n3,n2)),n4)) by Th25;

      

       A3: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n3,n4,n1))

      proof

        set q2 = ( crossover (p2,p1,n2,n3));

        set q1 = ( crossover (p1,p2,n2,n3));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n3,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n1));

        hence thesis;

      end;

      

       A4: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n4,n3,n2))

      proof

        set q2 = ( crossover (p2,p1,n1,n3));

        set q1 = ( crossover (p1,p2,n1,n3));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n3,n2)),n4)) by Th25

        .= ( crossover (q1,q2,n2,n4))

        .= ( crossover (q1,q2,n4,n2)) by Th13

        .= ( crossover (( crossover (p1,p2,n1,n3,n4)),( crossover (p2,p1,n1,n3,n4)),n2))

        .= ( crossover (( crossover (p1,p2,n1,n4,n3)),( crossover (p2,p1,n1,n3,n4)),n2)) by Th25

        .= ( crossover (( crossover (p1,p2,n1,n4,n3)),( crossover (p2,p1,n1,n4,n3)),n2)) by Th25;

        hence thesis;

      end;

      

       A5: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4,n3,n2,n1))

      proof

        set q2 = ( crossover (p2,p1,n3,n2));

        set q1 = ( crossover (p1,p2,n3,n2));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n2,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n3,n2,n4)),( crossover (p2,p1,n3,n2,n4)),n1))

        .= ( crossover (( crossover (p1,p2,n4,n3,n2)),( crossover (p2,p1,n3,n2,n4)),n1)) by Th26

        .= ( crossover (( crossover (p1,p2,n4,n3,n2)),( crossover (p2,p1,n4,n3,n2)),n1)) by Th26;

        hence thesis;

      end;

      

       A6: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n1,n4,n3))

      proof

        set q2 = ( crossover (p2,p1,n2,n1));

        set q1 = ( crossover (p1,p2,n2,n1));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (q1,q2,n3,n4))

        .= ( crossover (q1,q2,n4,n3)) by Th13

        .= ( crossover (( crossover (p1,p2,n2,n1,n4)),( crossover (p2,p1,n2,n1,n4)),n3));

        hence thesis;

      end;

      

       A7: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n4,n2,n3,n1))

      proof

        set q2 = ( crossover (p2,p1,n2,n3));

        set q1 = ( crossover (p1,p2,n2,n3));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n3,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n1))

        .= ( crossover (( crossover (p1,p2,n4,n2,n3)),( crossover (p2,p1,n2,n3,n4)),n1)) by Th26

        .= ( crossover (( crossover (p1,p2,n4,n2,n3)),( crossover (p2,p1,n4,n2,n3)),n1)) by Th26;

        hence thesis;

      end;

      

       A8: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n1,n3,n4,n2))

      proof

        set q2 = ( crossover (p2,p1,n1,n3));

        set q1 = ( crossover (p1,p2,n1,n3));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n1,n3,n2)),( crossover (p2,p1,n1,n3,n2)),n4)) by Th25

        .= ( crossover (q1,q2,n2,n4))

        .= ( crossover (q1,q2,n4,n2)) by Th13

        .= ( crossover (( crossover (q1,q2,n4)),( crossover (q2,q1,n4)),n2));

        hence thesis;

      end;

      

       A9: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n2,n4,n1))

      proof

        set q2 = ( crossover (p2,p1,n3,n2));

        set q1 = ( crossover (p1,p2,n3,n2));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n2,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n3,n2,n4)),( crossover (p2,p1,n3,n2,n4)),n1));

        hence thesis;

      end;

      

       A10: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4,n1,n3))

      proof

        set q2 = ( crossover (p2,p1,n2,n1));

        set q1 = ( crossover (p1,p2,n2,n1));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (q1,q2,n3,n4))

        .= ( crossover (q1,q2,n4,n3)) by Th13

        .= ( crossover (( crossover (p1,p2,n2,n1,n4)),( crossover (p2,p1,n2,n1,n4)),n3))

        .= ( crossover (( crossover (p1,p2,n2,n4,n1)),( crossover (p2,p1,n2,n1,n4)),n3)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n4,n1)),( crossover (p2,p1,n2,n4,n1)),n3)) by Th25;

        hence thesis;

      end;

      

       A11: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4,n2,n1))

      proof

        set q2 = ( crossover (p2,p1,n3,n2));

        set q1 = ( crossover (p1,p2,n3,n2));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n2,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n3,n2,n4)),( crossover (p2,p1,n3,n2,n4)),n1))

        .= ( crossover (( crossover (p1,p2,n3,n4,n2)),( crossover (p2,p1,n3,n2,n4)),n1)) by Th25

        .= ( crossover (( crossover (p1,p2,n3,n4,n2)),( crossover (p2,p1,n3,n4,n2)),n1)) by Th25;

        hence thesis;

      end;

      

       A12: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th26

      .= ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th26

      .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n3,n2,n1)),( crossover (p2,p1,n3,n2,n1)),n4)) by Th25;

      

       A13: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n3,n4,n1,n2))

      proof

        set q2 = ( crossover (p2,p1,n3,n1));

        set q1 = ( crossover (p1,p2,n3,n1));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th26

        .= ( crossover (( crossover (p1,p2,n3,n1,n2)),( crossover (p2,p1,n3,n1,n2)),n4)) by Th26

        .= ( crossover (q1,q2,n2,n4))

        .= ( crossover (q1,q2,n4,n2)) by Th13

        .= ( crossover (( crossover (p1,p2,n3,n1,n4)),( crossover (p2,p1,n3,n1,n4)),n2))

        .= ( crossover (( crossover (p1,p2,n3,n4,n1)),( crossover (p2,p1,n3,n1,n4)),n2)) by Th25

        .= ( crossover (( crossover (p1,p2,n3,n4,n1)),( crossover (p2,p1,n3,n4,n1)),n2)) by Th25;

        hence thesis;

      end;

      

       A14: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (p1,p2,n2,n4,n3,n1))

      proof

        set q2 = ( crossover (p2,p1,n2,n3));

        set q1 = ( crossover (p1,p2,n2,n3));

        ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n3,n1)),n4)) by Th25

        .= ( crossover (q1,q2,n1,n4))

        .= ( crossover (q1,q2,n4,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n1))

        .= ( crossover (( crossover (p1,p2,n2,n4,n3)),( crossover (p2,p1,n2,n3,n4)),n1)) by Th25

        .= ( crossover (( crossover (p1,p2,n2,n4,n3)),( crossover (p2,p1,n2,n4,n3)),n1)) by Th25;

        hence thesis;

      end;

      

       A15: ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25;

      ( crossover (p1,p2,n1,n2,n3,n4)) = ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n1,n2,n3)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n2,n1,n3)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n1,n3)),n4)) by Th25

      .= ( crossover (( crossover (p1,p2,n2,n3,n1)),( crossover (p2,p1,n2,n3,n1)),n4)) by Th25;

      hence thesis by A2, A15, A1, A8, A4, A6, A3, A10, A14, A12, A9, A13, A11, A7, A5;

    end;

    theorem :: GENEALG1:38

    

     Th38: ( crossover (p1,p2,n1,n1,n3,n4)) = ( crossover (p1,p2,n3,n4)) & ( crossover (p1,p2,n1,n2,n1,n4)) = ( crossover (p1,p2,n2,n4)) & ( crossover (p1,p2,n1,n2,n3,n1)) = ( crossover (p1,p2,n2,n3)) & ( crossover (p1,p2,n1,n2,n2,n4)) = ( crossover (p1,p2,n1,n4)) & ( crossover (p1,p2,n1,n2,n3,n2)) = ( crossover (p1,p2,n1,n3)) & ( crossover (p1,p2,n1,n2,n3,n3)) = ( crossover (p1,p2,n1,n2))

    proof

      ( crossover (p1,p2,n1,n1,n3,n4)) = ( crossover (( crossover (p1,p2,n3)),( crossover (p2,p1,n1,n1,n3)),n4)) by Th27

      .= ( crossover (( crossover (p1,p2,n3)),( crossover (p2,p1,n3)),n4)) by Th27;

      hence ( crossover (p1,p2,n1,n1,n3,n4)) = ( crossover (p1,p2,n3,n4));

      ( crossover (p1,p2,n1,n2,n1,n4)) = ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n1,n2,n1)),n4)) by Th27

      .= ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n2)),n4)) by Th27;

      hence ( crossover (p1,p2,n1,n2,n1,n4)) = ( crossover (p1,p2,n2,n4));

      ( crossover (p1,p2,n1,n2,n3,n1)) = ( crossover (p1,p2,n1,n1,n2,n3)) by Th37

      .= ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n1,n1,n2)),n3)) by Th27

      .= ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n2)),n3)) by Th27;

      hence ( crossover (p1,p2,n1,n2,n3,n1)) = ( crossover (p1,p2,n2,n3));

      ( crossover (p1,p2,n1,n2,n2,n4)) = ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n2,n2)),n4)) by Th27

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n4)) by Th27;

      hence ( crossover (p1,p2,n1,n2,n2,n4)) = ( crossover (p1,p2,n1,n4));

      ( crossover (p1,p2,n1,n2,n3,n2)) = ( crossover (p1,p2,n1,n2,n2,n3)) by Th37

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n2,n2)),n3)) by Th27

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n3)) by Th27;

      hence ( crossover (p1,p2,n1,n2,n3,n2)) = ( crossover (p1,p2,n1,n3));

      ( crossover (p1,p2,n1,n2,n3,n3)) = ( crossover (p1,p2,n1,n3,n3,n2)) by Th37

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n3,n3)),n2)) by Th27

      .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n2)) by Th27;

      hence thesis;

    end;

    theorem :: GENEALG1:39

    ( crossover (p1,p2,n1,n1,n3,n3)) = p1 & ( crossover (p1,p2,n1,n2,n1,n2)) = p1 & ( crossover (p1,p2,n1,n2,n2,n1)) = p1

    proof

      ( crossover (p1,p2,n1,n1,n3,n3)) = ( crossover (p1,p2,n3,n3)) by Th38;

      hence ( crossover (p1,p2,n1,n1,n3,n3)) = p1 by Th12;

      ( crossover (p1,p2,n1,n2,n1,n2)) = ( crossover (p1,p2,n2,n2)) by Th38;

      hence ( crossover (p1,p2,n1,n2,n1,n2)) = p1 by Th12;

      ( crossover (p1,p2,n1,n2,n2,n1)) = ( crossover (p1,p2,n2,n2)) by Th38;

      hence thesis by Th12;

    end;

    begin

    theorem :: GENEALG1:40

    

     Th40: ( crossover (p1,p2,n1,n2,n3,n4,n5)) is Individual of S

    proof

      reconsider q1 = ( crossover (p1,p2,n1,n2,n3,n4)), q2 = ( crossover (p2,p1,n1,n2,n3,n4)) as Individual of S;

      ( crossover (q1,q2,n5)) is Individual of S;

      hence thesis;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n1, n2, n3, n4, n5;

      :: original: crossover

      redefine

      func crossover (p1,p2,n1,n2,n3,n4,n5) -> Individual of S ;

      correctness by Th40;

    end

    theorem :: GENEALG1:41

    

     Th41: ( crossover (p1,p2, 0 ,n2,n3,n4,n5)) = ( crossover (p2,p1,n2,n3,n4,n5)) & ( crossover (p1,p2,n1, 0 ,n3,n4,n5)) = ( crossover (p2,p1,n1,n3,n4,n5)) & ( crossover (p1,p2,n1,n2, 0 ,n4,n5)) = ( crossover (p2,p1,n1,n2,n4,n5)) & ( crossover (p1,p2,n1,n2,n3, 0 ,n5)) = ( crossover (p2,p1,n1,n2,n3,n5)) & ( crossover (p1,p2,n1,n2,n3,n4, 0 )) = ( crossover (p2,p1,n1,n2,n3,n4))

    proof

      

       A1: ( crossover (p1,p2,n1,n2,n3,n4, 0 )) = ( crossover (( crossover (p1,p2,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)), 0 ));

      

       A2: ( crossover (p1,p2,n1, 0 ,n3,n4,n5)) = ( crossover (( crossover (p2,p1,n1,n3,n4)),( crossover (p2,p1,n1, 0 ,n3,n4)),n5)) by Th29

      .= ( crossover (( crossover (p2,p1,n1,n3,n4)),( crossover (p1,p2,n1,n3,n4)),n5)) by Th29;

      

       A3: ( crossover (p1,p2,n1,n2,n3, 0 ,n5)) = ( crossover (( crossover (p2,p1,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3, 0 )),n5)) by Th29

      .= ( crossover (( crossover (p2,p1,n1,n2,n3)),( crossover (p1,p2,n1,n2,n3)),n5)) by Th29;

      

       A4: ( crossover (p1,p2,n1,n2, 0 ,n4,n5)) = ( crossover (( crossover (p2,p1,n1,n2,n4)),( crossover (p2,p1,n1,n2, 0 ,n4)),n5)) by Th29

      .= ( crossover (( crossover (p2,p1,n1,n2,n4)),( crossover (p1,p2,n1,n2,n4)),n5)) by Th29;

      ( crossover (p1,p2, 0 ,n2,n3,n4,n5)) = ( crossover (( crossover (p2,p1,n2,n3,n4)),( crossover (p2,p1, 0 ,n2,n3,n4)),n5)) by Th29

      .= ( crossover (( crossover (p2,p1,n2,n3,n4)),( crossover (p1,p2,n2,n3,n4)),n5)) by Th29;

      hence thesis by A2, A4, A3, A1, Th4;

    end;

    theorem :: GENEALG1:42

    ( crossover (p1,p2, 0 , 0 ,n3,n4,n5)) = ( crossover (p1,p2,n3,n4,n5)) & ( crossover (p1,p2, 0 ,n2, 0 ,n4,n5)) = ( crossover (p1,p2,n2,n4,n5)) & ( crossover (p1,p2, 0 ,n2,n3, 0 ,n5)) = ( crossover (p1,p2,n2,n3,n5)) & ( crossover (p1,p2, 0 ,n2,n3,n4, 0 )) = ( crossover (p1,p2,n2,n3,n4)) & ( crossover (p1,p2,n1, 0 , 0 ,n4,n5)) = ( crossover (p1,p2,n1,n4,n5)) & ( crossover (p1,p2,n1, 0 ,n3, 0 ,n5)) = ( crossover (p1,p2,n1,n3,n5)) & ( crossover (p1,p2,n1, 0 ,n3,n4, 0 )) = ( crossover (p1,p2,n1,n3,n4)) & ( crossover (p1,p2,n1,n2, 0 , 0 ,n5)) = ( crossover (p1,p2,n1,n2,n5)) & ( crossover (p1,p2,n1,n2, 0 ,n4, 0 )) = ( crossover (p1,p2,n1,n2,n4)) & ( crossover (p1,p2,n1,n2,n3, 0 , 0 )) = ( crossover (p1,p2,n1,n2,n3))

    proof

      

       A1: ( crossover (p1,p2, 0 ,n2,n3,n4, 0 )) = ( crossover (( crossover (p1,p2, 0 ,n2,n3,n4)),( crossover (p1,p2,n2,n3,n4)), 0 )) & ( crossover (p1,p2,n1, 0 ,n3,n4, 0 )) = ( crossover (( crossover (p1,p2,n1, 0 ,n3,n4)),( crossover (p1,p2,n1,n3,n4)), 0 )) by Th29;

      

       A2: ( crossover (p1,p2,n1,n2, 0 ,n4, 0 )) = ( crossover (( crossover (p1,p2,n1,n2, 0 ,n4)),( crossover (p1,p2,n1,n2,n4)), 0 )) & ( crossover (p1,p2,n1,n2,n3, 0 , 0 )) = ( crossover (( crossover (p1,p2,n1,n2,n3, 0 )),( crossover (p1,p2,n1,n2,n3)), 0 )) by Th29;

      

       A3: ( crossover (p1,p2,n1, 0 ,n3, 0 ,n5)) = ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1, 0 ,n3, 0 )),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n3)),n5)) by Th30;

      

       A4: ( crossover (p1,p2,n1, 0 , 0 ,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n4)),( crossover (p2,p1,n1, 0 , 0 ,n4)),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n1,n4)),( crossover (p2,p1,n1,n4)),n5)) by Th30;

      

       A5: ( crossover (p1,p2,n1,n2, 0 , 0 ,n5)) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2, 0 , 0 )),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)),n5)) by Th30;

      

       A6: ( crossover (p1,p2, 0 ,n2,n3, 0 ,n5)) = ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1, 0 ,n2,n3, 0 )),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n2,n3)),n5)) by Th30;

      

       A7: ( crossover (p1,p2, 0 ,n2, 0 ,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1, 0 ,n2, 0 ,n4)),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n2,n4)),n5)) by Th30;

      ( crossover (p1,p2, 0 , 0 ,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1, 0 , 0 ,n3,n4)),n5)) by Th30

      .= ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n3,n4)),n5)) by Th30;

      hence thesis by A7, A6, A4, A3, A1, A5, A2, Th4;

    end;

    theorem :: GENEALG1:43

    ( crossover (p1,p2, 0 , 0 , 0 ,n4,n5)) = ( crossover (p2,p1,n4,n5)) & ( crossover (p1,p2, 0 , 0 ,n3, 0 ,n5)) = ( crossover (p2,p1,n3,n5)) & ( crossover (p1,p2, 0 , 0 ,n3,n4, 0 )) = ( crossover (p2,p1,n3,n4)) & ( crossover (p1,p2, 0 ,n2, 0 , 0 ,n5)) = ( crossover (p2,p1,n2,n5)) & ( crossover (p1,p2, 0 ,n2, 0 ,n4, 0 )) = ( crossover (p2,p1,n2,n4)) & ( crossover (p1,p2, 0 ,n2,n3, 0 , 0 )) = ( crossover (p2,p1,n2,n3)) & ( crossover (p1,p2,n1, 0 , 0 , 0 ,n5)) = ( crossover (p2,p1,n1,n5)) & ( crossover (p1,p2,n1, 0 , 0 ,n4, 0 )) = ( crossover (p2,p1,n1,n4)) & ( crossover (p1,p2,n1, 0 ,n3, 0 , 0 )) = ( crossover (p2,p1,n1,n3)) & ( crossover (p1,p2,n1,n2, 0 , 0 , 0 )) = ( crossover (p2,p1,n1,n2))

    proof

      

       A1: ( crossover (p1,p2, 0 , 0 ,n3,n4, 0 )) = ( crossover (( crossover (p1,p2, 0 , 0 ,n3,n4)),( crossover (p2,p1,n3,n4)), 0 )) & ( crossover (p1,p2, 0 ,n2, 0 ,n4, 0 )) = ( crossover (( crossover (p1,p2, 0 ,n2, 0 ,n4)),( crossover (p2,p1,n2,n4)), 0 )) by Th30;

      

       A2: ( crossover (p1,p2, 0 ,n2,n3, 0 , 0 )) = ( crossover (( crossover (p1,p2, 0 ,n2,n3, 0 )),( crossover (p2,p1,n2,n3)), 0 )) & ( crossover (p1,p2,n1, 0 , 0 ,n4, 0 )) = ( crossover (( crossover (p1,p2,n1, 0 , 0 ,n4)),( crossover (p2,p1,n1,n4)), 0 )) by Th30;

      

       A3: ( crossover (p1,p2, 0 , 0 ,n3, 0 ,n5)) = ( crossover (( crossover (p2,p1,n3)),( crossover (p2,p1, 0 , 0 ,n3, 0 )),n5)) by Th31

      .= ( crossover (( crossover (p2,p1,n3)),( crossover (p1,p2,n3)),n5)) by Th31;

      

       A4: ( crossover (p1,p2,n1, 0 ,n3, 0 , 0 )) = ( crossover (( crossover (p1,p2,n1, 0 ,n3, 0 )),( crossover (p2,p1,n1,n3)), 0 )) & ( crossover (p1,p2,n1,n2, 0 , 0 , 0 )) = ( crossover (( crossover (p1,p2,n1,n2, 0 , 0 )),( crossover (p2,p1,n1,n2)), 0 )) by Th30;

      

       A5: ( crossover (p1,p2,n1, 0 , 0 , 0 ,n5)) = ( crossover (( crossover (p2,p1,n1)),( crossover (p2,p1,n1, 0 , 0 , 0 )),n5)) by Th31

      .= ( crossover (( crossover (p2,p1,n1)),( crossover (p1,p2,n1)),n5)) by Th31;

      

       A6: ( crossover (p1,p2, 0 ,n2, 0 , 0 ,n5)) = ( crossover (( crossover (p2,p1,n2)),( crossover (p2,p1, 0 ,n2, 0 , 0 )),n5)) by Th31

      .= ( crossover (( crossover (p2,p1,n2)),( crossover (p1,p2,n2)),n5)) by Th31;

      ( crossover (p1,p2, 0 , 0 , 0 ,n4,n5)) = ( crossover (( crossover (p2,p1,n4)),( crossover (p2,p1, 0 , 0 , 0 ,n4)),n5)) by Th31

      .= ( crossover (( crossover (p2,p1,n4)),( crossover (p1,p2,n4)),n5)) by Th31;

      hence thesis by A3, A6, A1, A5, A2, A4, Th4;

    end;

    theorem :: GENEALG1:44

    ( crossover (p1,p2, 0 , 0 , 0 , 0 ,n5)) = ( crossover (p1,p2,n5)) & ( crossover (p1,p2, 0 , 0 , 0 ,n4, 0 )) = ( crossover (p1,p2,n4)) & ( crossover (p1,p2, 0 , 0 ,n3, 0 , 0 )) = ( crossover (p1,p2,n3)) & ( crossover (p1,p2, 0 ,n2, 0 , 0 , 0 )) = ( crossover (p1,p2,n2)) & ( crossover (p1,p2,n1, 0 , 0 , 0 , 0 )) = ( crossover (p1,p2,n1))

    proof

      

       A1: ( crossover (p1,p2, 0 , 0 ,n3, 0 , 0 )) = ( crossover (( crossover (p1,p2, 0 , 0 ,n3, 0 )),( crossover (p1,p2,n3)), 0 )) & ( crossover (p1,p2, 0 ,n2, 0 , 0 , 0 )) = ( crossover (( crossover (p1,p2, 0 ,n2, 0 , 0 )),( crossover (p1,p2,n2)), 0 )) by Th31;

      

       A2: ( crossover (p1,p2,n1, 0 , 0 , 0 , 0 )) = ( crossover (( crossover (p1,p2,n1, 0 , 0 , 0 )),( crossover (p1,p2,n1)), 0 )) by Th31;

      ( crossover (p1,p2, 0 , 0 , 0 , 0 ,n5)) = ( crossover (p1,( crossover (p2,p1, 0 , 0 , 0 , 0 )),n5)) & ( crossover (p1,p2, 0 , 0 , 0 ,n4, 0 )) = ( crossover (( crossover (p1,p2, 0 , 0 , 0 ,n4)),( crossover (p1,p2,n4)), 0 )) by Th31, Th32;

      hence thesis by A1, A2, Th4, Th32;

    end;

    theorem :: GENEALG1:45

    ( crossover (p1,p2, 0 , 0 , 0 , 0 , 0 )) = p2

    proof

      ( crossover (p1,p2, 0 , 0 , 0 , 0 , 0 )) = ( crossover (( crossover (p1,p2, 0 , 0 , 0 , 0 )),p2, 0 )) by Th32;

      hence thesis by Th4;

    end;

    theorem :: GENEALG1:46

    

     Th46: (n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n4,n5))) & (n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n4,n5))) & (n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n4,n5))) & (n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3,n5))) & (n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3,n4)))

    proof

      

       A1: n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3,n4))

      proof

        assume n5 >= ( len p1);

        then n5 >= ( len S) by Def1;

        then

         A2: n5 >= ( len ( crossover (p1,p2,n1,n2,n3,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5));

        hence thesis by A2, Th5;

      end;

      

       A3: n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n4,n5))

      proof

        assume

         A4: n2 >= ( len p1);

        then n2 >= ( len S) by Def1;

        then

         A5: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A4, Th33

        .= ( crossover (( crossover (p1,p2,n1,n3,n4)),( crossover (p2,p1,n1,n3,n4)),n5)) by A5, Th33;

        hence thesis;

      end;

      

       A6: n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3,n5))

      proof

        assume

         A7: n4 >= ( len p1);

        then n4 >= ( len S) by Def1;

        then

         A8: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A7, Th33

        .= ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3)),n5)) by A8, Th33;

        hence thesis;

      end;

      

       A9: n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n4,n5))

      proof

        assume

         A10: n3 >= ( len p1);

        then n3 >= ( len S) by Def1;

        then

         A11: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A10, Th33

        .= ( crossover (( crossover (p1,p2,n1,n2,n4)),( crossover (p2,p1,n1,n2,n4)),n5)) by A11, Th33;

        hence thesis;

      end;

      n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n4,n5))

      proof

        assume

         A12: n1 >= ( len p1);

        then n1 >= ( len S) by Def1;

        then

         A13: n1 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A12, Th33

        .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n5)) by A13, Th33;

        hence thesis;

      end;

      hence thesis by A3, A9, A6, A1;

    end;

    theorem :: GENEALG1:47

    (n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n4,n5))) & (n1 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n4,n5))) & (n1 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n5))) & (n1 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n4))) & (n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n4,n5))) & (n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n5))) & (n2 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n4))) & (n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n5))) & (n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n4))) & (n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3)))

    proof

      

       A1: n2 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n4))

      proof

        assume that

         A2: n2 >= ( len p1) and

         A3: n5 >= ( len p1);

        n5 >= ( len S) by A3, Def1;

        then

         A4: n5 >= ( len ( crossover (p1,p2,n1,n3,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A2, Th33;

        hence thesis by A4, Th5;

      end;

      

       A5: n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n4))

      proof

        assume that

         A6: n3 >= ( len p1) and

         A7: n5 >= ( len p1);

        n5 >= ( len S) by A7, Def1;

        then

         A8: n5 >= ( len ( crossover (p1,p2,n1,n2,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A6, Th33;

        hence thesis by A8, Th5;

      end;

      

       A9: n1 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n5))

      proof

        assume that

         A10: n1 >= ( len p1) and

         A11: n4 >= ( len p1);

        n1 >= ( len S) by A10, Def1;

        then

         A12: n1 >= ( len p2) by Def1;

        n4 >= ( len S) by A11, Def1;

        then

         A13: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A10, A11, Th34

        .= ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n2,n3)),n5)) by A12, A13, Th34;

        hence thesis;

      end;

      

       A14: n1 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n4,n5))

      proof

        assume that

         A15: n1 >= ( len p1) and

         A16: n3 >= ( len p1);

        n1 >= ( len S) by A15, Def1;

        then

         A17: n1 >= ( len p2) by Def1;

        n3 >= ( len S) by A16, Def1;

        then

         A18: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A15, A16, Th34

        .= ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n2,n4)),n5)) by A17, A18, Th34;

        hence thesis;

      end;

      

       A19: n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3,n5))

      proof

        assume that

         A20: n2 >= ( len p1) and

         A21: n4 >= ( len p1);

        n2 >= ( len S) by A20, Def1;

        then

         A22: n2 >= ( len p2) by Def1;

        n4 >= ( len S) by A21, Def1;

        then

         A23: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A20, A21, Th34

        .= ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n3)),n5)) by A22, A23, Th34;

        hence thesis;

      end;

      

       A24: n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n4,n5))

      proof

        assume that

         A25: n2 >= ( len p1) and

         A26: n3 >= ( len p1);

        n2 >= ( len S) by A25, Def1;

        then

         A27: n2 >= ( len p2) by Def1;

        n3 >= ( len S) by A26, Def1;

        then

         A28: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A25, A26, Th34

        .= ( crossover (( crossover (p1,p2,n1,n4)),( crossover (p2,p1,n1,n4)),n5)) by A27, A28, Th34;

        hence thesis;

      end;

      

       A29: n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n5))

      proof

        assume that

         A30: n3 >= ( len p1) and

         A31: n4 >= ( len p1);

        n3 >= ( len S) by A30, Def1;

        then

         A32: n3 >= ( len p2) by Def1;

        n4 >= ( len S) by A31, Def1;

        then

         A33: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A30, A31, Th34

        .= ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2)),n5)) by A32, A33, Th34;

        hence thesis;

      end;

      

       A34: n1 >= ( len p1) & n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n4,n5))

      proof

        assume that

         A35: n1 >= ( len p1) and

         A36: n2 >= ( len p1);

        n1 >= ( len S) by A35, Def1;

        then

         A37: n1 >= ( len p2) by Def1;

        n2 >= ( len S) by A36, Def1;

        then

         A38: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A35, A36, Th34

        .= ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n3,n4)),n5)) by A37, A38, Th34;

        hence thesis;

      end;

      

       A39: n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2,n3))

      proof

        assume that

         A40: n4 >= ( len p1) and

         A41: n5 >= ( len p1);

        n5 >= ( len S) by A41, Def1;

        then

         A42: n5 >= ( len ( crossover (p1,p2,n1,n2,n3))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A40, Th33;

        hence thesis by A42, Th5;

      end;

      n1 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3,n4))

      proof

        assume that

         A43: n1 >= ( len p1) and

         A44: n5 >= ( len p1);

        n5 >= ( len S) by A44, Def1;

        then

         A45: n5 >= ( len ( crossover (p1,p2,n2,n3,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A43, Th33;

        hence thesis by A45, Th5;

      end;

      hence thesis by A34, A14, A9, A24, A19, A1, A29, A5, A39;

    end;

    theorem :: GENEALG1:48

    (n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n4,n5))) & (n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n5))) & (n1 >= ( len p1) & n2 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n4))) & (n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n5))) & (n1 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n4))) & (n1 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3))) & (n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n5))) & (n2 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n4))) & (n2 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3))) & (n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2)))

    proof

      

       A1: n1 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n4))

      proof

        assume that

         A2: n1 >= ( len p1) & n3 >= ( len p1) and

         A3: n5 >= ( len p1);

        n5 >= ( len S) by A3, Def1;

        then

         A4: n5 >= ( len ( crossover (p1,p2,n2,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A2, Th34;

        hence thesis by A4, Th5;

      end;

      

       A5: n1 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n3))

      proof

        assume that

         A6: n1 >= ( len p1) & n4 >= ( len p1) and

         A7: n5 >= ( len p1);

        n5 >= ( len S) by A7, Def1;

        then

         A8: n5 >= ( len ( crossover (p1,p2,n2,n3))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A6, Th34;

        hence thesis by A8, Th5;

      end;

      

       A9: n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n5))

      proof

        assume that

         A10: n1 >= ( len p1) and

         A11: n2 >= ( len p1) and

         A12: n4 >= ( len p1);

        n1 >= ( len S) by A10, Def1;

        then

         A13: n1 >= ( len p2) by Def1;

        n4 >= ( len S) by A12, Def1;

        then

         A14: n4 >= ( len p2) by Def1;

        n2 >= ( len S) by A11, Def1;

        then

         A15: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A10, A11, A12, Th35

        .= ( crossover (( crossover (p1,p2,n3)),( crossover (p2,p1,n3)),n5)) by A13, A15, A14, Th35;

        hence thesis;

      end;

      

       A16: n2 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n3))

      proof

        assume that

         A17: n2 >= ( len p1) & n4 >= ( len p1) and

         A18: n5 >= ( len p1);

        n5 >= ( len S) by A18, Def1;

        then

         A19: n5 >= ( len ( crossover (p1,p2,n1,n3))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A17, Th34;

        hence thesis by A19, Th5;

      end;

      

       A20: n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n5))

      proof

        assume that

         A21: n2 >= ( len p1) and

         A22: n3 >= ( len p1) and

         A23: n4 >= ( len p1);

        n2 >= ( len S) by A21, Def1;

        then

         A24: n2 >= ( len p2) by Def1;

        n4 >= ( len S) by A23, Def1;

        then

         A25: n4 >= ( len p2) by Def1;

        n3 >= ( len S) by A22, Def1;

        then

         A26: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A21, A22, A23, Th35

        .= ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1)),n5)) by A24, A26, A25, Th35;

        hence thesis;

      end;

      

       A27: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n4,n5))

      proof

        assume that

         A28: n1 >= ( len p1) and

         A29: n2 >= ( len p1) and

         A30: n3 >= ( len p1);

        n1 >= ( len S) by A28, Def1;

        then

         A31: n1 >= ( len p2) by Def1;

        n3 >= ( len S) by A30, Def1;

        then

         A32: n3 >= ( len p2) by Def1;

        n2 >= ( len S) by A29, Def1;

        then

         A33: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A28, A29, A30, Th35

        .= ( crossover (( crossover (p1,p2,n4)),( crossover (p2,p1,n4)),n5)) by A31, A33, A32, Th35;

        hence thesis;

      end;

      

       A34: n2 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n4))

      proof

        assume that

         A35: n2 >= ( len p1) & n3 >= ( len p1) and

         A36: n5 >= ( len p1);

        n5 >= ( len S) by A36, Def1;

        then

         A37: n5 >= ( len ( crossover (p1,p2,n1,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A35, Th34;

        hence thesis by A37, Th5;

      end;

      

       A38: n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n5))

      proof

        assume that

         A39: n1 >= ( len p1) and

         A40: n3 >= ( len p1) and

         A41: n4 >= ( len p1);

        n1 >= ( len S) by A39, Def1;

        then

         A42: n1 >= ( len p2) by Def1;

        n4 >= ( len S) by A41, Def1;

        then

         A43: n4 >= ( len p2) by Def1;

        n3 >= ( len S) by A40, Def1;

        then

         A44: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A39, A40, A41, Th35

        .= ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n2)),n5)) by A42, A44, A43, Th35;

        hence thesis;

      end;

      

       A45: n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1,n2))

      proof

        assume that

         A46: n3 >= ( len p1) & n4 >= ( len p1) and

         A47: n5 >= ( len p1);

        n5 >= ( len S) by A47, Def1;

        then

         A48: n5 >= ( len ( crossover (p1,p2,n1,n2))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1,n2)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A46, Th34;

        hence thesis by A48, Th5;

      end;

      n1 >= ( len p1) & n2 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n4))

      proof

        assume that

         A49: n1 >= ( len p1) & n2 >= ( len p1) and

         A50: n5 >= ( len p1);

        n5 >= ( len S) by A50, Def1;

        then

         A51: n5 >= ( len ( crossover (p1,p2,n3,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A49, Th34;

        hence thesis by A51, Th5;

      end;

      hence thesis by A27, A9, A38, A1, A5, A20, A34, A16, A45;

    end;

    theorem :: GENEALG1:49

    (n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n5))) & (n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n4))) & (n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3))) & (n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2))) & (n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1)))

    proof

      

       A1: n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3))

      proof

        assume that

         A2: n1 >= ( len p1) & n2 >= ( len p1) & n4 >= ( len p1) and

         A3: n5 >= ( len p1);

        n5 >= ( len S) by A3, Def1;

        then

         A4: n5 >= ( len ( crossover (p1,p2,n3))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A2, Th35;

        hence thesis by A4, Th5;

      end;

      

       A5: n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2))

      proof

        assume that

         A6: n1 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) and

         A7: n5 >= ( len p1);

        n5 >= ( len S) by A7, Def1;

        then

         A8: n5 >= ( len ( crossover (p1,p2,n2))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A6, Th35;

        hence thesis by A8, Th5;

      end;

      

       A9: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n5))

      proof

        assume that

         A10: n1 >= ( len p1) and

         A11: n2 >= ( len p1) and

         A12: n3 >= ( len p1) and

         A13: n4 >= ( len p1);

        n1 >= ( len S) by A10, Def1;

        then

         A14: n1 >= ( len p2) by Def1;

        n3 >= ( len S) by A12, Def1;

        then

         A15: n3 >= ( len p2) by Def1;

        n2 >= ( len S) by A11, Def1;

        then

         A16: n2 >= ( len p2) by Def1;

        n4 >= ( len S) by A13, Def1;

        then

         A17: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A10, A11, A12, A13, Th36;

        hence thesis by A14, A16, A15, A17, Th36;

      end;

      

       A18: n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n1))

      proof

        assume that

         A19: n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) and

         A20: n5 >= ( len p1);

        n5 >= ( len S) by A20, Def1;

        then

         A21: n5 >= ( len ( crossover (p1,p2,n1))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n1)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A19, Th35;

        hence thesis by A21, Th5;

      end;

      n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n4))

      proof

        assume that

         A22: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) and

         A23: n5 >= ( len p1);

        n5 >= ( len S) by A23, Def1;

        then

         A24: n5 >= ( len ( crossover (p1,p2,n4))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A22, Th35;

        hence thesis by A24, Th5;

      end;

      hence thesis by A9, A1, A5, A18;

    end;

    theorem :: GENEALG1:50

    n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) & n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5)) = p1

    proof

      assume that

       A1: n1 >= ( len p1) & n2 >= ( len p1) & n3 >= ( len p1) & n4 >= ( len p1) and

       A2: n5 >= ( len p1);

      ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,( crossover (p2,p1,n1,n2,n3,n4)),n5)) by A1, Th36;

      hence thesis by A2, Th5;

    end;

    theorem :: GENEALG1:51

    

     Th51: ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n2,n1,n3,n4,n5)) & ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n3,n2,n1,n4,n5)) & ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n4,n2,n3,n1,n5)) & ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n5,n2,n3,n4,n1))

    proof

      

       A1: ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3,n2,n1,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by Th37

      .= ( crossover (( crossover (p1,p2,n3,n2,n1,n4)),( crossover (p2,p1,n3,n2,n1,n4)),n5)) by Th37;

      

       A2: ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n4,n2,n3,n1)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by Th37

      .= ( crossover (( crossover (p1,p2,n4,n2,n3,n1)),( crossover (p2,p1,n4,n2,n3,n1)),n5)) by Th37;

      

       A3: ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (p1,p2,n5,n2,n3,n4,n1))

      proof

        set q2 = ( crossover (p2,p1,n2,n3,n4));

        set q1 = ( crossover (p1,p2,n2,n3,n4));

        

         A4: ( crossover (p1,p2,n2,n3,n4,n5)) = ( crossover (q1,q2,n5));

        ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n3,n4,n1)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by Th37

        .= ( crossover (( crossover (p1,p2,n2,n3,n4,n1)),( crossover (p2,p1,n2,n3,n4,n1)),n5)) by Th37

        .= ( crossover (q1,q2,n1,n5))

        .= ( crossover (q1,q2,n5,n1)) by Th13

        .= ( crossover (( crossover (p1,p2,n5,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4,n5)),n1)) by A4, Th37

        .= ( crossover (( crossover (p1,p2,n5,n2,n3,n4)),( crossover (p2,p1,n5,n2,n3,n4)),n1)) by Th37;

        hence thesis;

      end;

      ( crossover (p1,p2,n1,n2,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n1,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n5)) by Th37

      .= ( crossover (( crossover (p1,p2,n2,n1,n3,n4)),( crossover (p2,p1,n2,n1,n3,n4)),n5)) by Th37;

      hence thesis by A1, A2, A3;

    end;

    theorem :: GENEALG1:52

    

     Th52: ( crossover (p1,p2,n1,n1,n3,n4,n5)) = ( crossover (p1,p2,n3,n4,n5)) & ( crossover (p1,p2,n1,n2,n1,n4,n5)) = ( crossover (p1,p2,n2,n4,n5)) & ( crossover (p1,p2,n1,n2,n3,n1,n5)) = ( crossover (p1,p2,n2,n3,n5)) & ( crossover (p1,p2,n1,n2,n3,n4,n1)) = ( crossover (p1,p2,n2,n3,n4))

    proof

      set q1 = ( crossover (p1,p2,n2,n3,n4));

      set q2 = ( crossover (p2,p1,n2,n3,n4));

      ( crossover (p1,p2,n1,n1,n3,n4,n5)) = ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n1,n1,n3,n4)),n5)) by Th38

      .= ( crossover (( crossover (p1,p2,n3,n4)),( crossover (p2,p1,n3,n4)),n5)) by Th38;

      hence ( crossover (p1,p2,n1,n1,n3,n4,n5)) = ( crossover (p1,p2,n3,n4,n5));

      ( crossover (p1,p2,n1,n2,n1,n4,n5)) = ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n1,n2,n1,n4)),n5)) by Th38

      .= ( crossover (( crossover (p1,p2,n2,n4)),( crossover (p2,p1,n2,n4)),n5)) by Th38;

      hence ( crossover (p1,p2,n1,n2,n1,n4,n5)) = ( crossover (p1,p2,n2,n4,n5));

      ( crossover (p1,p2,n1,n2,n3,n1,n5)) = ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n1,n2,n3,n1)),n5)) by Th38

      .= ( crossover (( crossover (p1,p2,n2,n3)),( crossover (p2,p1,n2,n3)),n5)) by Th38;

      hence ( crossover (p1,p2,n1,n2,n3,n1,n5)) = ( crossover (p1,p2,n2,n3,n5));

      ( crossover (p1,p2,n1,n2,n3,n4,n1)) = ( crossover (( crossover (p1,p2,n2,n3,n4,n1)),( crossover (p2,p1,n1,n2,n3,n4)),n1)) by Th37

      .= ( crossover (( crossover (p1,p2,n2,n3,n4,n1)),( crossover (p2,p1,n2,n3,n4,n1)),n1)) by Th37

      .= ( crossover (q1,q2,n1,n1));

      hence thesis by Th12;

    end;

    begin

    theorem :: GENEALG1:53

    

     Th53: ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) is Individual of S

    proof

      reconsider q1 = ( crossover (p1,p2,n1,n2,n3,n4,n5)), q2 = ( crossover (p2,p1,n1,n2,n3,n4,n5)) as Individual of S;

      ( crossover (q1,q2,n6)) is Individual of S;

      hence thesis;

    end;

    definition

      let S be Gene-Set, p1,p2 be Individual of S, n1, n2, n3, n4, n5, n6;

      :: original: crossover

      redefine

      func crossover (p1,p2,n1,n2,n3,n4,n5,n6) -> Individual of S ;

      correctness by Th53;

    end

    theorem :: GENEALG1:54

    ( crossover (p1,p2, 0 ,n2,n3,n4,n5,n6)) = ( crossover (p2,p1,n2,n3,n4,n5,n6)) & ( crossover (p1,p2,n1, 0 ,n3,n4,n5,n6)) = ( crossover (p2,p1,n1,n3,n4,n5,n6)) & ( crossover (p1,p2,n1,n2, 0 ,n4,n5,n6)) = ( crossover (p2,p1,n1,n2,n4,n5,n6)) & ( crossover (p1,p2,n1,n2,n3, 0 ,n5,n6)) = ( crossover (p2,p1,n1,n2,n3,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n4, 0 ,n6)) = ( crossover (p2,p1,n1,n2,n3,n4,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5, 0 )) = ( crossover (p2,p1,n1,n2,n3,n4,n5))

    proof

      ( crossover (p1,p2, 0 ,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p2,p1,n2,n3,n4,n5)),( crossover (p2,p1, 0 ,n2,n3,n4,n5)),n6)) by Th41

      .= ( crossover (( crossover (p2,p1,n2,n3,n4,n5)),( crossover (p1,p2,n2,n3,n4,n5)),n6)) by Th41;

      hence ( crossover (p1,p2, 0 ,n2,n3,n4,n5,n6)) = ( crossover (p2,p1,n2,n3,n4,n5,n6));

      ( crossover (p1,p2,n1, 0 ,n3,n4,n5,n6)) = ( crossover (( crossover (p2,p1,n1,n3,n4,n5)),( crossover (p2,p1,n1, 0 ,n3,n4,n5)),n6)) by Th41

      .= ( crossover (( crossover (p2,p1,n1,n3,n4,n5)),( crossover (p1,p2,n1,n3,n4,n5)),n6)) by Th41;

      hence ( crossover (p1,p2,n1, 0 ,n3,n4,n5,n6)) = ( crossover (p2,p1,n1,n3,n4,n5,n6));

      ( crossover (p1,p2,n1,n2, 0 ,n4,n5,n6)) = ( crossover (( crossover (p2,p1,n1,n2,n4,n5)),( crossover (p2,p1,n1,n2, 0 ,n4,n5)),n6)) by Th41

      .= ( crossover (( crossover (p2,p1,n1,n2,n4,n5)),( crossover (p1,p2,n1,n2,n4,n5)),n6)) by Th41;

      hence ( crossover (p1,p2,n1,n2, 0 ,n4,n5,n6)) = ( crossover (p2,p1,n1,n2,n4,n5,n6));

      ( crossover (p1,p2,n1,n2,n3, 0 ,n5,n6)) = ( crossover (( crossover (p2,p1,n1,n2,n3,n5)),( crossover (p2,p1,n1,n2,n3, 0 ,n5)),n6)) by Th41

      .= ( crossover (( crossover (p2,p1,n1,n2,n3,n5)),( crossover (p1,p2,n1,n2,n3,n5)),n6)) by Th41;

      hence ( crossover (p1,p2,n1,n2,n3, 0 ,n5,n6)) = ( crossover (p2,p1,n1,n2,n3,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n4, 0 ,n6)) = ( crossover (( crossover (p2,p1,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4, 0 )),n6)) by Th41

      .= ( crossover (( crossover (p2,p1,n1,n2,n3,n4)),( crossover (p1,p2,n1,n2,n3,n4)),n6)) by Th41;

      hence ( crossover (p1,p2,n1,n2,n3,n4, 0 ,n6)) = ( crossover (p2,p1,n1,n2,n3,n4,n6));

      

      thus ( crossover (p1,p2,n1,n2,n3,n4,n5, 0 )) = ( crossover (( crossover (p1,p2,n1,n2,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)), 0 ))

      .= ( crossover (p2,p1,n1,n2,n3,n4,n5)) by Th4;

    end;

    theorem :: GENEALG1:55

    (n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n2,n3,n4,n5,n6))) & (n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n3,n4,n5,n6))) & (n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n4,n5,n6))) & (n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n5,n6))) & (n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n4,n6))) & (n6 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n4,n5)))

    proof

      

       A1: n6 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n4,n5))

      proof

        assume n6 >= ( len p1);

        then n6 >= ( len S) by Def1;

        then

         A2: n6 >= ( len ( crossover (p1,p2,n1,n2,n3,n4,n5))) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n1,n2,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6));

        hence thesis by A2, Th5;

      end;

      

       A3: n2 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n3,n4,n5,n6))

      proof

        assume

         A4: n2 >= ( len p1);

        then n2 >= ( len S) by Def1;

        then

         A5: n2 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n1,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by A4, Th46

        .= ( crossover (( crossover (p1,p2,n1,n3,n4,n5)),( crossover (p2,p1,n1,n3,n4,n5)),n6)) by A5, Th46;

        hence thesis;

      end;

      

       A6: n5 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n4,n6))

      proof

        assume

         A7: n5 >= ( len p1);

        then n5 >= ( len S) by Def1;

        then

         A8: n5 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by A7, Th46

        .= ( crossover (( crossover (p1,p2,n1,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4)),n6)) by A8, Th46;

        hence thesis;

      end;

      

       A9: n4 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n3,n5,n6))

      proof

        assume

         A10: n4 >= ( len p1);

        then n4 >= ( len S) by Def1;

        then

         A11: n4 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n1,n2,n3,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by A10, Th46

        .= ( crossover (( crossover (p1,p2,n1,n2,n3,n5)),( crossover (p2,p1,n1,n2,n3,n5)),n6)) by A11, Th46;

        hence thesis;

      end;

      

       A12: n3 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n1,n2,n4,n5,n6))

      proof

        assume

         A13: n3 >= ( len p1);

        then n3 >= ( len S) by Def1;

        then

         A14: n3 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n1,n2,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by A13, Th46

        .= ( crossover (( crossover (p1,p2,n1,n2,n4,n5)),( crossover (p2,p1,n1,n2,n4,n5)),n6)) by A14, Th46;

        hence thesis;

      end;

      n1 >= ( len p1) implies ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n2,n3,n4,n5,n6))

      proof

        assume

         A15: n1 >= ( len p1);

        then n1 >= ( len S) by Def1;

        then

         A16: n1 >= ( len p2) by Def1;

        ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n2,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by A15, Th46

        .= ( crossover (( crossover (p1,p2,n2,n3,n4,n5)),( crossover (p2,p1,n2,n3,n4,n5)),n6)) by A16, Th46;

        hence thesis;

      end;

      hence thesis by A3, A12, A9, A6, A1;

    end;

    theorem :: GENEALG1:56

    

     Th56: ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n2,n1,n3,n4,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n3,n2,n1,n4,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n4,n2,n3,n1,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n5,n2,n3,n4,n1,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n6,n2,n3,n4,n5,n1))

    proof

      set q1 = ( crossover (p1,p2,n5,n2,n3,n4));

      set q2 = ( crossover (p2,p1,n5,n2,n3,n4));

      

       A1: ( crossover (p1,p2,n5,n2,n3,n4,n6)) = ( crossover (q1,q2,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n2,n1,n3,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by Th51

      .= ( crossover (( crossover (p1,p2,n2,n1,n3,n4,n5)),( crossover (p2,p1,n2,n1,n3,n4,n5)),n6)) by Th51;

      hence ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n2,n1,n3,n4,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n3,n2,n1,n4,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by Th51

      .= ( crossover (( crossover (p1,p2,n3,n2,n1,n4,n5)),( crossover (p2,p1,n3,n2,n1,n4,n5)),n6)) by Th51;

      hence ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n3,n2,n1,n4,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n4,n2,n3,n1,n5)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by Th51

      .= ( crossover (( crossover (p1,p2,n4,n2,n3,n1,n5)),( crossover (p2,p1,n4,n2,n3,n1,n5)),n6)) by Th51;

      hence ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n4,n2,n3,n1,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n5,n2,n3,n4,n1)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by Th51

      .= ( crossover (( crossover (p1,p2,n5,n2,n3,n4,n1)),( crossover (p2,p1,n5,n2,n3,n4,n1)),n6)) by Th51;

      hence ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (p1,p2,n5,n2,n3,n4,n1,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n5,n2,n3,n4,n1)),( crossover (p2,p1,n1,n2,n3,n4,n5)),n6)) by Th51

      .= ( crossover (( crossover (p1,p2,n5,n2,n3,n4,n1)),( crossover (p2,p1,n5,n2,n3,n4,n1)),n6)) by Th51

      .= ( crossover (q1,q2,n1,n6))

      .= ( crossover (q1,q2,n6,n1)) by Th13

      .= ( crossover (( crossover (p1,p2,n6,n2,n3,n4,n5)),( crossover (p2,p1,n5,n2,n3,n4,n6)),n1)) by A1, Th51

      .= ( crossover (( crossover (p1,p2,n6,n2,n3,n4,n5)),( crossover (p2,p1,n6,n2,n3,n4,n5)),n1)) by Th51;

      hence thesis;

    end;

    theorem :: GENEALG1:57

    ( crossover (p1,p2,n1,n1,n3,n4,n5,n6)) = ( crossover (p1,p2,n3,n4,n5,n6)) & ( crossover (p1,p2,n1,n2,n1,n4,n5,n6)) = ( crossover (p1,p2,n2,n4,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n1,n5,n6)) = ( crossover (p1,p2,n2,n3,n5,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n1,n6)) = ( crossover (p1,p2,n2,n3,n4,n6)) & ( crossover (p1,p2,n1,n2,n3,n4,n5,n1)) = ( crossover (p1,p2,n2,n3,n4,n5))

    proof

      ( crossover (p1,p2,n1,n1,n3,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n3,n4,n5)),( crossover (p2,p1,n1,n1,n3,n4,n5)),n6)) by Th52

      .= ( crossover (( crossover (p1,p2,n3,n4,n5)),( crossover (p2,p1,n3,n4,n5)),n6)) by Th52;

      hence ( crossover (p1,p2,n1,n1,n3,n4,n5,n6)) = ( crossover (p1,p2,n3,n4,n5,n6));

      ( crossover (p1,p2,n1,n2,n1,n4,n5,n6)) = ( crossover (( crossover (p1,p2,n2,n4,n5)),( crossover (p2,p1,n1,n2,n1,n4,n5)),n6)) by Th52

      .= ( crossover (( crossover (p1,p2,n2,n4,n5)),( crossover (p2,p1,n2,n4,n5)),n6)) by Th52;

      hence ( crossover (p1,p2,n1,n2,n1,n4,n5,n6)) = ( crossover (p1,p2,n2,n4,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n1,n5,n6)) = ( crossover (( crossover (p1,p2,n2,n3,n5)),( crossover (p2,p1,n1,n2,n3,n1,n5)),n6)) by Th52

      .= ( crossover (( crossover (p1,p2,n2,n3,n5)),( crossover (p2,p1,n2,n3,n5)),n6)) by Th52;

      hence ( crossover (p1,p2,n1,n2,n3,n1,n5,n6)) = ( crossover (p1,p2,n2,n3,n5,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n1,n6)) = ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4,n1)),n6)) by Th52

      .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n6)) by Th52;

      hence ( crossover (p1,p2,n1,n2,n3,n4,n1,n6)) = ( crossover (p1,p2,n2,n3,n4,n6));

      ( crossover (p1,p2,n1,n2,n3,n4,n5,n1)) = ( crossover (p1,p2,n5,n2,n3,n4,n1,n1)) by Th56

      .= ( crossover (p1,p2,n1,n2,n3,n4,n1,n5)) by Th56

      .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n1,n2,n3,n4,n1)),n5)) by Th52

      .= ( crossover (( crossover (p1,p2,n2,n3,n4)),( crossover (p2,p1,n2,n3,n4)),n5)) by Th52;

      hence thesis;

    end;