ballot_1.miz



    begin

    reserve D,D1,D2 for non empty set,

d,d1,d2 for XFinSequence of D,

n,k,i,j for Nat;

    theorem :: BALLOT_1:1

    

     Th1: ( XFS2FS (d | n)) = (( XFS2FS d) | n) by AFINSQ_2: 84;

    theorem :: BALLOT_1:2

    

     Th2: ( rng d) = ( rng ( XFS2FS d)) by AFINSQ_1: 97;

    theorem :: BALLOT_1:3

    

     Th3: for d1 be XFinSequence of D1, d2 be XFinSequence of D2 st d1 = d2 holds ( XFS2FS d1) = ( XFS2FS d2)

    proof

      let d1 be XFinSequence of D1, d2 be XFinSequence of D2;

      assume

       A1: d1 = d2;

      set Xd1 = ( XFS2FS d1), Xd2 = ( XFS2FS d2);

      

       A2: ( len Xd1) = ( len d1) by AFINSQ_1:def 9;

      for i st 1 <= i & i <= ( len d1) holds (Xd1 . i) = (Xd2 . i)

      proof

        let i such that

         A3: 1 <= i and

         A4: i <= ( len d1);

        (Xd1 . i) = (d1 . (i -' 1)) by AFINSQ_1:def 9, A3, A4;

        hence thesis by AFINSQ_1:def 9, A3, A4, A1;

      end;

      hence thesis by A2, AFINSQ_1:def 9, A1;

    end;

    theorem :: BALLOT_1:4

    

     Th4: ( XFS2FS d1) = ( XFS2FS d2) implies d1 = d2

    proof

      assume

       A1: ( XFS2FS d1) = ( XFS2FS d2);

      set Xd1 = ( XFS2FS d1), Xd2 = ( XFS2FS d2);

      

       A2: ( len Xd1) = ( len d1) by AFINSQ_1:def 9;

      

       A3: ( len Xd2) = ( len d2) by AFINSQ_1:def 9;

      for i st i < ( len d1) holds (d1 . i) = (d2 . i)

      proof

        let i such that

         A4: i < ( len d1);

        

         A5: (i + 1) <= ( len d1) by A4, NAT_1: 13;

        

         A6: ((i + 1) -' 1) = i by NAT_D: 34;

        then (d1 . i) = (Xd1 . (i + 1)) by NAT_1: 11, A5, AFINSQ_1:def 9;

        hence thesis by A6, NAT_1: 11, A5, A2, A3, A1, AFINSQ_1:def 9;

      end;

      hence thesis by A2, A3, A1, AFINSQ_1: 9;

    end;

    theorem :: BALLOT_1:5

    for D be set holds for d be FinSequence of D holds ( XFS2FS ( FS2XFS d)) = d;

    theorem :: BALLOT_1:6

    

     Th6: for f be FinSequence, x,y be object st ( rng f) c= {x, y} & x <> y holds (( card (f " {x})) + ( card (f " {y}))) = ( len f)

    proof

      let f be FinSequence, A,B be object;

      

       A1: ( {A} \/ {B}) = {A, B} by ENUMSET1: 1;

      assume that

       A2: ( rng f) c= {A, B} and

       A3: A <> B;

      (f " ( rng f)) c= (f " {A, B}) by A2, RELAT_1: 143;

      

      then

       A4: ( dom f) = (f " {A, B}) by RELAT_1: 132, RELAT_1: 134

      .= ((f " {A}) \/ (f " {B})) by RELAT_1: 140, A1;

      (f " {A}) misses (f " {B})

      proof

        assume (f " {A}) meets (f " {B});

        then

        consider x be object such that

         A5: x in (f " {A}) and

         A6: x in (f " {B}) by XBOOLE_0: 3;

        

         A7: (f . x) in {A} by A5, FUNCT_1:def 7;

        

         A8: (f . x) in {B} by A6, FUNCT_1:def 7;

        (f . x) = A by A7, TARSKI:def 1;

        hence thesis by A8, TARSKI:def 1, A3;

      end;

      

      hence (( card (f " {A})) + ( card (f " {B}))) = ( card ( dom f)) by A4, CARD_2: 40

      .= ( card ( Seg ( len f))) by FINSEQ_1:def 3

      .= ( len f) by FINSEQ_1: 57;

    end;

    theorem :: BALLOT_1:7

    

     Th7: for f,g be Function st f is one-to-one holds for x be object st x in ( dom f) holds ( Coim ((f * g),(f . x))) = ( Coim (g,x))

    proof

      let f,g be Function such that

       A1: f is one-to-one;

      let x be object such that

       A2: x in ( dom f);

      set fg = (f * g);

      thus ( Coim (fg,(f . x))) c= ( Coim (g,x))

      proof

        let z be object;

        assume

         A3: z in ( Coim (fg,(f . x)));

        then

         A4: z in ( dom fg) by FUNCT_1:def 7;

        

         A5: (fg . z) in {(f . x)} by A3, FUNCT_1:def 7;

        

         A6: z in ( dom g) by A4, FUNCT_1: 11;

        

         A7: (g . z) in ( dom f) by A4, FUNCT_1: 11;

        

         A8: (fg . z) = (f . (g . z)) by A4, FUNCT_1: 12;

        (fg . z) = (f . x) by A5, TARSKI:def 1;

        then (g . z) = x by A7, A8, A2, A1;

        then (g . z) in {x} by TARSKI:def 1;

        hence thesis by FUNCT_1:def 7, A6;

      end;

      let z be object;

      assume

       A9: z in ( Coim (g,x));

      then

       A10: z in ( dom g) by FUNCT_1:def 7;

      (g . z) in {x} by A9, FUNCT_1:def 7;

      then

       A11: (g . z) = x by TARSKI:def 1;

      then

       A12: (fg . z) = (f . x) by FUNCT_1: 13, A10;

      

       A13: z in ( dom fg) by A11, A2, FUNCT_1: 11, A10;

      (f . x) in {(f . x)} by TARSKI:def 1;

      hence thesis by A12, A13, FUNCT_1:def 7;

    end;

    theorem :: BALLOT_1:8

    

     Th21: for r be Real, f be real-valued FinSequence st ( rng f) c= { 0 , r} holds ( Sum f) = (r * ( card (f " {r})))

    proof

      let r be Real;

      defpred P[ Nat] means for f be real-valued FinSequence st ( len f) = $1 & ( rng f) c= { 0 , r} holds ( Sum f) = (r * ( card (f " {r})));

      

       A1: P[ 0 ]

      proof

        let f be real-valued FinSequence such that

         A2: ( len f) = 0 and ( rng f) c= { 0 , r};

        

         A3: f = {} by A2;

        then (f " {r}) = {} ;

        hence thesis by A3, RVSUM_1: 72;

      end;

      

       A4: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A5: P[n];

        set n1 = (n + 1);

        let f be real-valued FinSequence such that

         A6: ( len f) = n1 and

         A7: ( rng f) c= { 0 , r};

        ( rng f) c= REAL ;

        then

        reconsider F = f as FinSequence of REAL by FINSEQ_1:def 4;

        set fn = (F | n), FF = <*(f . n1)*>;

        

         A8: f = (fn ^ FF) by A6, FINSEQ_3: 55;

        then

         A9: ( Sum f) = (( Sum fn) + (F . n1)) by RVSUM_1: 74;

        ( rng fn) c= ( rng f) by RELAT_1: 70;

        then

         A10: ( rng fn) c= { 0 , r} by A7;

        

         A11: ( len fn) = n by NAT_1: 11, A6, FINSEQ_1: 59;

        then

         A12: ( Sum fn) = (r * ( card (fn " {r}))) by A10, A5;

        

         A13: ( dom FF) = ( Seg 1) by FINSEQ_1: 38;

        ( rng FF) = {(F . n1)} by FINSEQ_1: 38;

        then

         A14: FF = (( Seg 1) --> (F . n1)) by A13, FUNCOP_1: 9;

        

         A15: ( card (f " {r})) = (( card (fn " {r})) + ( card (FF " {r}))) by FINSEQ_3: 57, A8;

        1 <= n1 by NAT_1: 11;

        then n1 in ( dom F) by A6, FINSEQ_3: 25;

        then

         A16: (F . n1) in ( rng F) by FUNCT_1:def 3;

        per cases ;

          suppose

           A17: (F . n1) <> r;

          then not (F . n1) in {r} by TARSKI:def 1;

          then

           A18: (FF " {r}) = {} by A14, FUNCOP_1: 16;

          (F . n1) = 0 by A17, A16, A7, TARSKI:def 2;

          hence thesis by A11, A10, A5, A9, A15, A18;

        end;

          suppose

           A19: (F . n1) = r;

          then (FF " {r}) = ( Seg 1) by A14, FUNCOP_1: 15;

          then ( card (FF " {r})) = 1 by FINSEQ_1: 57;

          hence thesis by A12, A9, A15, A19;

        end;

      end;

      

       A20: for n holds P[n] from NAT_1:sch 2( A1, A4);

      let f be real-valued FinSequence;

       P[( len f)] by A20;

      hence thesis;

    end;

    begin

    reserve A,B for object,

v for Element of ((n + k) -tuples_on {A, B}),

f,g for FinSequence;

    definition

      let A, n, B, k;

      :: BALLOT_1:def1

      func Election (A,n,B,k) -> Subset of ((n + k) -tuples_on {A, B}) means

      : Def1: v in it iff ( card (v " {A})) = n;

      existence

      proof

        set V = { v : ( card (v " {A})) = n };

        V c= ((n + k) -tuples_on {A, B})

        proof

          let x be object;

          assume x in V;

          then ex v st v = x & ( card (v " {A})) = n;

          hence thesis;

        end;

        then

        reconsider V as Subset of ((n + k) -tuples_on {A, B});

        take V;

        let v;

        hereby

          assume v in V;

          then ex v1 be Element of ((n + k) -tuples_on {A, B}) st v = v1 & ( card (v1 " {A})) = n;

          hence ( card (v " {A})) = n;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let V1,V2 be Subset of ((n + k) -tuples_on {A, B});

        assume that

         A1: v in V1 iff ( card (v " {A})) = n and

         A2: v in V2 iff ( card (v " {A})) = n;

        hereby

          let x be object;

          assume

           A3: x in V1;

          then

          reconsider v = x as Element of ((n + k) -tuples_on {A, B});

          ( card (v " {A})) = n by A1, A3;

          hence x in V2 by A2;

        end;

        let x be object;

        assume

         A4: x in V2;

        then

        reconsider v = x as Element of ((n + k) -tuples_on {A, B});

        ( card (v " {A})) = n by A2, A4;

        hence x in V1 by A1;

      end;

    end

    registration

      let A, n, B, k;

      cluster ( Election (A,n,B,k)) -> finite;

      coherence ;

    end

    theorem :: BALLOT_1:9

    ( Election (A,n,A, 0 )) = {(n |-> A)}

    proof

      

       A1: {A, A} = {A} by ENUMSET1: 29;

      thus ( Election (A,n,A, 0 )) c= {(n |-> A)}

      proof

        let x be object;

        assume

         A2: x in ( Election (A,n,A, 0 ));

        then

        reconsider v = x as Element of ((n + 0 ) -tuples_on {A}) by ENUMSET1: 29;

        

         A3: ( card (v " {A})) = n by A2, Def1;

        

         A4: ( len v) = n by CARD_1:def 7;

        per cases ;

          suppose ( rng v) = {} ;

          then v = ( {} --> {A});

          then v = (n |-> A) by A3;

          hence thesis by TARSKI:def 1;

        end;

          suppose ( rng v) <> {} ;

          then v = (( dom v) --> A) by ZFMISC_1: 33, FUNCOP_1: 9;

          then v = (n |-> A) by A4, FINSEQ_1:def 3;

          hence thesis by TARSKI:def 1;

        end;

      end;

      A in {A} by TARSKI:def 1;

      then

      reconsider nA = (n |-> A) as Element of (n -tuples_on {A, A}) by A1, FINSEQ_2: 112;

      (nA " {A}) = ( Seg n) by FUNCOP_1: 15;

      then ( card (nA " {A})) = n by FINSEQ_1: 57;

      then nA in ( Election (A,n,A, 0 )) by Def1;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: BALLOT_1:10

    

     ElectionEmpty: k > 0 implies ( Election (A,n,A,k)) is empty

    proof

      assume

       A1: k > 0 ;

      assume ( Election (A,n,A,k)) is non empty;

      then

      consider v be object such that

       A2: v in ( Election (A,n,A,k));

      reconsider v as Element of ((n + k) -tuples_on {A}) by A2, ENUMSET1: 29;

      

       A3: ( card ( dom v)) = (n + k) by CARD_1:def 7;

      (v " ( rng v)) c= (v " {A}) by RELAT_1: 143;

      then (v " {A}) = ( dom v) by RELAT_1: 134, RELAT_1: 132;

      then (n + k) = n by A3, Def1, A2;

      hence contradiction by A1;

    end;

    registration

      let A, n;

      let k be non empty Nat;

      cluster ( Election (A,n,A,k)) -> empty;

      coherence

      proof

        k > 0 ;

        hence thesis by ElectionEmpty;

      end;

    end

    theorem :: BALLOT_1:11

    

     Th10: ( Election (A,n,B,k)) = ( Choose (( Seg (n + k)),n,A,B))

    proof

      thus ( Election (A,n,B,k)) c= ( Choose (( Seg (n + k)),n,A,B))

      proof

        let x be object;

        assume

         A1: x in ( Election (A,n,B,k));

        then

        reconsider v = x as Element of ((n + k) -tuples_on {A, B});

        

         A2: ( rng v) c= {A, B};

        ( len v) = (n + k) by CARD_1:def 7;

        then ( dom v) = ( Seg (n + k)) by FINSEQ_1:def 3;

        then

        reconsider V = v as Function of ( Seg (n + k)), {A, B} by FUNCT_2: 2, A2;

        ( card (v " {A})) = n by A1, Def1;

        then V in ( Choose (( Seg (n + k)),n,A,B)) by CARD_FIN:def 1;

        hence thesis;

      end;

      let x be object;

      assume x in ( Choose (( Seg (n + k)),n,A,B));

      then

      consider f be Function of ( Seg (n + k)), {A, B} such that

       A3: f = x and

       A4: ( card (f " {A})) = n by CARD_FIN:def 1;

      

       A5: ( rng f) c= {A, B};

      

       A6: ( dom f) = ( Seg (n + k)) by FUNCT_2:def 1;

      then

      reconsider f as FinSequence by FINSEQ_1:def 2;

      reconsider f as FinSequence of {A, B} by A5, FINSEQ_1:def 4;

      (n + k) in NAT by ORDINAL1:def 12;

      then ( len f) = (n + k) by FINSEQ_1:def 3, A6;

      then f is Element of ((n + k) -tuples_on {A, B}) by FINSEQ_2: 92;

      hence x in ( Election (A,n,B,k)) by A3, A4, Def1;

    end;

    theorem :: BALLOT_1:12

    

     Th11: A <> B implies (v in ( Election (A,n,B,k)) iff ( card (v " {B})) = k)

    proof

      assume

       A1: A <> B;

      

       A2: ( rng v) c= {A, B};

      

       A3: ( len v) = (n + k) by CARD_1:def 7;

      

       A4: (( card (v " {A})) + ( card (v " {B}))) = ( len v) by Th6, A2, A1;

      thus v in ( Election (A,n,B,k)) implies ( card (v " {B})) = k

      proof

        assume v in ( Election (A,n,B,k));

        then ( card (v " {A})) = n by Def1;

        hence thesis by A4, A3;

      end;

      assume ( card (v " {B})) = k;

      hence v in ( Election (A,n,B,k)) by A4, A3, Def1;

    end;

    theorem :: BALLOT_1:13

    

     Th12: A <> B implies ( card ( Election (A,n,B,k))) = ((n + k) choose n)

    proof

      assume

       A1: A <> B;

      

      thus ( card ( Election (A,n,B,k))) = ( card ( Choose (( Seg (n + k)),n,A,B))) by Th10

      .= (( card ( Seg (n + k))) choose n) by A1, CARD_FIN: 16

      .= ((n + k) choose n) by FINSEQ_1: 57;

    end;

    begin

    definition

      let A, n, B, k;

      let v be FinSequence;

      :: BALLOT_1:def2

      attr v is A,n,B,k -dominated-election means v in ( Election (A,n,B,k)) & for i st i > 0 holds ( card ((v | i) " {A})) > ( card ((v | i) " {B}));

    end

    theorem :: BALLOT_1:14

    

     Th13: f is A, n, B, k -dominated-election implies A <> B

    proof

      assume

       A1: f is A, n, B, k -dominated-election;

      then

      reconsider f as Element of ((n + k) -tuples_on {A, B});

      (( len f) + 1) >= ( len f) by NAT_1: 13;

      then (f | (( len f) + 1)) = f by FINSEQ_1: 58;

      then ( card (f " {A})) > ( card (f " {B})) by A1;

      hence thesis;

    end;

    theorem :: BALLOT_1:15

    

     Th14: f is A, n, B, k -dominated-election implies n > k

    proof

      assume

       A1: f is A, n, B, k -dominated-election;

      then

      reconsider f as Element of ((n + k) -tuples_on {A, B});

      (( len f) + 1) >= ( len f) by NAT_1: 13;

      then

       A2: (f | (( len f) + 1)) = f by FINSEQ_1: 58;

      

       A3: A <> B by A1, Th13;

      

       A4: ( card (f " {A})) = n by A1, Def1;

      ( card (f " {B})) = k by A1, A3, Th11;

      hence thesis by A2, A1, A4;

    end;

    theorem :: BALLOT_1:16

    

     Th15: A <> B & n > 0 implies (n |-> A) is A, n, B, 0 -dominated-election

    proof

      set nA = (n |-> A);

      assume that

       A1: A <> B and

       A2: n > 0 ;

      A is Element of {A, B} by TARSKI:def 2;

      then

      reconsider nA as Element of ((n + 0 ) -tuples_on {A, B}) by FINSEQ_2: 112;

      (nA " ( rng nA)) c= (nA " {A}) by FUNCOP_1: 13, RELAT_1: 143;

      then ( dom nA) = (nA " {A}) by RELAT_1: 132, RELAT_1: 134;

      

      then ( card (nA " {A})) = ( card ( Seg ( len nA))) by FINSEQ_1:def 3

      .= ( len nA) by FINSEQ_1: 57

      .= n by CARD_1:def 7;

      hence (n |-> A) in ( Election (A,n,B, 0 )) by Def1;

      let i such that

       A3: i > 0 ;

      set nAi = (nA | i);

      

       A4: nAi = ((( Seg n) /\ ( Seg i)) --> A) by FUNCOP_1: 12;

      

       A5: not A in {B} by A1, TARSKI:def 1;

      per cases ;

        suppose i <= n;

        then (( Seg i) /\ ( Seg n)) = ( Seg i) by FINSEQ_1: 5, XBOOLE_1: 28;

        then

         A6: (nAi " {A}) = ( Seg i) by A4, FUNCOP_1: 15;

        (nAi " {B}) = {} by A5, FUNCOP_1: 16, A4;

        hence thesis by A6, A3;

      end;

        suppose i > n;

        then (( Seg i) /\ ( Seg n)) = ( Seg n) by FINSEQ_1: 5, XBOOLE_1: 28;

        then

         A7: (nAi " {A}) = ( Seg n) by A4, FUNCOP_1: 15;

        (nAi " {B}) = {} by A5, FUNCOP_1: 16, A4;

        hence thesis by A2, A7;

      end;

    end;

    theorem :: BALLOT_1:17

    

     Th16: f is A, n, B, k -dominated-election & i < (n - k) implies (f ^ (i |-> B)) is A, n, B, (k + i) -dominated-election

    proof

      set iB = (i |-> B);

      assume that

       A1: f is A, n, B, k -dominated-election and

       A2: i < (n - k);

      

       A3: A <> B by A1, Th13;

      

       A4: ( rng iB) c= {B} by FUNCOP_1: 13;

       {B} c= {A, B} by ZFMISC_1: 7;

      then ( rng iB) c= {A, B} by A4;

      then

      reconsider iB as FinSequence of {A, B} by FINSEQ_1:def 4;

      reconsider F = f as Element of ((n + k) -tuples_on {A, B}) by A1;

      set fB = (f ^ (i |-> B));

      

       A5: ( len f) = (n + k) by A1, CARD_1:def 7;

      

       A6: ( len (F ^ iB)) = ((n + k) + i) by CARD_1:def 7;

      then

      reconsider FB = (F ^ iB) as Element of ((n + (k + i)) -tuples_on {A, B}) by FINSEQ_2: 92;

      

       A7: not B in {A} by A3, TARSKI:def 1;

      then

       A8: (iB " {A}) = {} by FUNCOP_1: 16;

      

       A9: ( card (FB " {A})) = (( card (F " {A})) + ( card (iB " {A}))) by FINSEQ_3: 57;

      

       A10: ( card (F " {A})) = n by Def1, A1;

      hence fB in ( Election (A,n,B,(k + i))) by A9, A8, Def1;

      let j such that

       A11: j > 0 ;

      set FBj = (FB | j);

      

       A12: ( card (f " {B})) = k by A3, Th11, A1;

      

       A13: (i + k) < ((n - k) + k) by A2, XREAL_1: 6;

      per cases ;

        suppose j <= (n + k);

        then FBj = (f | j) by A5, FINSEQ_5: 22;

        hence ( card ((fB | j) " {A})) > ( card ((fB | j) " {B})) by A11, A1;

      end;

        suppose

         A14: j > (n + k) & j <= ((n + k) + i);

        then

        reconsider j1 = (j - (n + k)) as Nat by NAT_1: 21;

        

         A15: (j1 + (n + k)) <= (i + (n + k)) by A14;

        then

         A16: j1 <= i by XREAL_1: 6;

        (( Seg i) /\ ( Seg j1)) = ( Seg j1) by A15, XREAL_1: 6, FINSEQ_1: 7;

        then

         A17: (iB | ( Seg j1)) = (( Seg j1) --> B) by FUNCOP_1: 12;

        

         A18: ((( Seg j1) --> B) " {A}) = {} by A7, FUNCOP_1: 16;

        

         A19: FBj = (FB | ( Seg (( len F) + j1))) by A5

        .= (F ^ (( Seg j1) --> B)) by A17, FINSEQ_6: 14;

        

        then

         A20: ( card (FBj " {A})) = (n + ( card ((( Seg j1) --> B) " {A}))) by A10, FINSEQ_3: 57

        .= n by A18;

        B in {B} by TARSKI:def 1;

        then ((( Seg j1) --> B) " {B}) = ( Seg j1) by FUNCOP_1: 14;

        

        then ( card (FBj " {B})) = (k + ( card ( Seg j1))) by A12, A19, FINSEQ_3: 57

        .= (k + j1) by FINSEQ_1: 57;

        then ( card (FBj " {B})) <= (k + i) by A16, XREAL_1: 6;

        hence ( card ((fB | j) " {A})) > ( card ((fB | j) " {B})) by A20, A13, XXREAL_0: 2;

      end;

        suppose j > ((n + k) + i);

        then

         A21: (FB | j) = FB by FINSEQ_1: 58, A6;

        

         A22: (iB " {A}) = {} by A7, FUNCOP_1: 16;

        B in {B} by TARSKI:def 1;

        then (iB " {B}) = ( Seg i) by FUNCOP_1: 14;

        

        then ( card (FB " {B})) = (k + ( card ( Seg i))) by A12, FINSEQ_3: 57

        .= (k + i) by FINSEQ_1: 57;

        hence ( card ((fB | j) " {A})) > ( card ((fB | j) " {B})) by A21, A22, A9, Def1, A1, A13;

      end;

    end;

    theorem :: BALLOT_1:18

    f is A, n, B, k -dominated-election & g is A, i, B, j -dominated-election implies (f ^ g) is A, (n + i), B, (k + j) -dominated-election

    proof

      assume that

       A1: f is A, n, B, k -dominated-election and

       A2: g is A, i, B, j -dominated-election;

      

       A3: A <> B by A1, Th13;

      reconsider F = f as Element of ((n + k) -tuples_on {A, B}) by A1;

      reconsider G = g as Element of ((i + j) -tuples_on {A, B}) by A2;

      

       A4: ( len F) = (n + k) by CARD_1:def 7;

      

       A5: ( len (F ^ G)) = ((n + k) + (i + j)) by CARD_1:def 7;

      then

      reconsider FG = (F ^ G) as Element of (((n + k) + (i + j)) -tuples_on {A, B}) by FINSEQ_2: 92;

      ( card (FG " {A})) = (( card (F " {A})) + ( card (G " {A}))) by FINSEQ_3: 57

      .= (n + ( card (G " {A}))) by A1, Def1

      .= (n + i) by A2, Def1;

      hence (f ^ g) in ( Election (A,(n + i),B,(k + j))) by Def1;

      let h be Nat such that

       A6: h > 0 ;

      per cases ;

        suppose h <= (n + k);

        then (FG | h) = (F | h) by A4, FINSEQ_5: 22;

        hence thesis by A1, A6;

      end;

        suppose

         A7: h > (n + k) & h <= (((n + k) + i) + j);

        then

        reconsider h1 = (h - (n + k)) as Nat by NAT_1: 21;

        

         A8: h1 <> 0 by A7;

        (h1 + ( len F)) = h by A4;

        then

         A9: (FG | h) = (F ^ (G | h1)) by FINSEQ_6: 14;

        

        then

         A10: ( card ((FG | h) " {A})) = (( card (F " {A})) + ( card ((G | h1) " {A}))) by FINSEQ_3: 57

        .= (n + ( card ((G | h1) " {A}))) by A1, Def1;

        

         A11: ( card ((FG | h) " {B})) = (( card (F " {B})) + ( card ((G | h1) " {B}))) by A9, FINSEQ_3: 57

        .= (k + ( card ((G | h1) " {B}))) by A3, A1, Th11;

        ( card ((G | h1) " {A})) > ( card ((G | h1) " {B})) by A8, A2;

        hence thesis by A10, A11, Th14, A1, XREAL_1: 8;

      end;

        suppose h > (((n + k) + i) + j);

        then

         A12: (FG | h) = FG by FINSEQ_1: 58, A5;

        

         A13: ( card (FG " {A})) = (( card (F " {A})) + ( card (G " {A}))) by FINSEQ_3: 57

        .= (n + ( card (G " {A}))) by A1, Def1

        .= (n + i) by A2, Def1;

        

         A14: ( card (FG " {B})) = (( card (F " {B})) + ( card (G " {B}))) by FINSEQ_3: 57

        .= (k + ( card (G " {B}))) by A3, A1, Th11

        .= (k + j) by A3, A2, Th11;

        n > k by Th14, A1;

        hence thesis by Th14, A2, A13, A14, XREAL_1: 8, A12;

      end;

    end;

    definition

      let A, n, B, k;

      :: BALLOT_1:def3

      func DominatedElection (A,n,B,k) -> Subset of ( Election (A,n,B,k)) means

      : Def3: f in it iff f is A, n, B, k -dominated-election;

      existence

      proof

        set BALL = { v : v is A, n, B, k -dominated-election };

        BALL c= ( Election (A,n,B,k))

        proof

          let x be object;

          assume x in BALL;

          then ex v st x = v & v is A, n, B, k -dominated-election;

          hence thesis;

        end;

        then

        reconsider BALL as Subset of ( Election (A,n,B,k));

        take BALL;

        let f;

        f in BALL implies f is A, n, B, k -dominated-election

        proof

          assume f in BALL;

          then ex v st f = v & v is A, n, B, k -dominated-election;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let B1,B2 be Subset of ( Election (A,n,B,k)) such that

         A1: f in B1 iff f is A, n, B, k -dominated-election and

         A2: f in B2 iff f is A, n, B, k -dominated-election;

        thus B1 c= B2 by A1, A2;

        let x be object;

        thus thesis by A2, A1;

      end;

    end

    theorem :: BALLOT_1:19

    

     Th18: A = B or n <= k implies ( DominatedElection (A,n,B,k)) is empty

    proof

      assume

       A1: A = B or n <= k;

      assume ( DominatedElection (A,n,B,k)) is non empty;

      then

      consider f be object such that

       A2: f in ( DominatedElection (A,n,B,k));

      f in ( Election (A,n,B,k)) by A2;

      then

      reconsider f as Element of ((n + k) -tuples_on {A, B});

      f is A, n, B, k -dominated-election by A2, Def3;

      hence thesis by Th13, Th14, A1;

    end;

    theorem :: BALLOT_1:20

    n > k & A <> B implies ((n |-> A) ^ (k |-> B)) in ( DominatedElection (A,n,B,k))

    proof

      assume that

       A1: n > k and

       A2: A <> B;

      k < (n - 0 ) by A1;

      then ((n |-> A) ^ (k |-> B)) is A, n, B, ( 0 + k) -dominated-election by Th16, A2, Th15;

      hence thesis by Def3;

    end;

    theorem :: BALLOT_1:21

    

     Th20: A <> B implies ( card ( DominatedElection (A,n,B,k))) = ( card ( DominatedElection ( 0 ,n,1,k)))

    proof

      assume

       A1: A <> B;

      set T = ((A,B) --> ( 0 ,1)), W = (( 0 ,1) --> (A,B));

      

       A2: ( dom T) = {A, B} by FUNCT_4: 62;

      

       A3: ( rng T) = { 0 , 1} by A1, FUNCT_4: 64;

      

       A4: ( rng W) = {A, B} by FUNCT_4: 64;

      

       A5: ( dom W) = { 0 , 1} by FUNCT_4: 62;

      

       A6: A is set by TARSKI: 1;

      

       A7: B is set by TARSKI: 1;

      

       A8: ( rng (A .--> 0 )) = { 0 } by A6, FUNCOP_1: 88;

      

       A9: ( rng (B .--> 1)) = {1} by A7, FUNCOP_1: 88;

      

       A10: ( rng ( 0 .--> A)) = {A} by A6, FUNCOP_1: 88;

      

       A11: ( rng (1 .--> B)) = {B} by A7, FUNCOP_1: 88;

      

       A12: ((A .--> 0 ) +* (B .--> 1)) is one-to-one by A8, A9, ZFMISC_1: 11, FUNCT_4: 92;

      

       A13: (( 0 .--> A) +* (1 .--> B)) is one-to-one by A10, A11, A1, ZFMISC_1: 11, FUNCT_4: 92;

      

       A14: T is one-to-one by A12, FUNCT_4:def 4;

      

       A15: W is one-to-one by A13, FUNCT_4:def 4;

      

       A16: (T . A) = 0 by A1, FUNCT_4: 63;

      

       A17: (T . B) = 1 by FUNCT_4: 63;

      

       A18: (W . 0 ) = A by FUNCT_4: 63;

      

       A19: (W . 1) = B by FUNCT_4: 63;

      defpred P[ object, object] means for f st f = $1 holds (T * f) = $2;

      

       A20: for x be object st x in ( DominatedElection (A,n,B,k)) holds ex y be object st y in ( DominatedElection ( 0 ,n,1,k)) & P[x, y]

      proof

        let x be object such that

         A21: x in ( DominatedElection (A,n,B,k));

        x in ( Election (A,n,B,k)) by A21;

        then

        reconsider f = x as Element of ((n + k) -tuples_on {A, B});

        

         A22: ( len f) = (n + k) by CARD_1:def 7;

        

         A23: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        ( rng f) c= {A, B};

        then

         A24: ( dom (T * f)) = ( Seg ( len f)) by A23, A2, RELAT_1: 27;

        

         A25: ( rng (T * f)) c= { 0 , 1} by A3, RELAT_1: 26;

        reconsider Tf = (T * f) as FinSequence;

        reconsider Tf as FinSequence of { 0 , 1} by A25, FINSEQ_1:def 4;

        ( len Tf) = ( len f) by A24, FINSEQ_1:def 3;

        then

        reconsider Tf as Element of ((n + k) -tuples_on { 0 , 1}) by A22, FINSEQ_2: 92;

        take Tf;

        Tf is 0 , n, 1, k -dominated-election

        proof

          

           A26: A in ( dom T) by A2, TARSKI:def 2;

          

           A27: B in ( dom T) by A2, TARSKI:def 2;

          ( Coim (Tf, 0 )) = ( Coim (f,A)) by A26, Th7, A14, A16;

          then ( card ( Coim (Tf, 0 ))) = n by A21, Def1;

          hence Tf in ( Election ( 0 ,n,1,k)) by Def1;

          let i such that

           A28: i > 0 ;

          

           A29: (Tf | i) = (T * (f | i)) by RELAT_1: 83;

          then

           A30: ( Coim ((Tf | i), 0 )) = ( Coim ((f | i),A)) by A26, Th7, A14, A16;

          

           A31: ( Coim ((Tf | i),1)) = ( Coim ((f | i),B)) by A29, A27, Th7, A14, A17;

          f is A, n, B, k -dominated-election by A21, Def3;

          hence thesis by A28, A30, A31;

        end;

        hence thesis by Def3;

      end;

      consider C be Function of ( DominatedElection (A,n,B,k)), ( DominatedElection ( 0 ,n,1,k)) such that

       A32: for x be object st x in ( DominatedElection (A,n,B,k)) holds P[x, (C . x)] from FUNCT_2:sch 1( A20);

      ( DominatedElection ( 0 ,n,1,k)) c= ( rng C)

      proof

        let x be object;

        assume

         A33: x in ( DominatedElection ( 0 ,n,1,k));

        then x in ( Election ( 0 ,n,1,k));

        then

        reconsider f = x as Element of ((n + k) -tuples_on { 0 , 1});

        

         A34: ( len f) = (n + k) by CARD_1:def 7;

        

         A35: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        

         A36: ( rng f) c= { 0 , 1};

        then

         A37: ( dom (W * f)) = ( Seg ( len f)) by A35, A5, RELAT_1: 27;

        

         A38: ( rng (W * f)) c= {A, B} by A4, RELAT_1: 26;

        reconsider Wf = (W * f) as FinSequence by A37, FINSEQ_1:def 2;

        reconsider Wf as FinSequence of {A, B} by A38, FINSEQ_1:def 4;

        ( len Wf) = ( len f) by A37, FINSEQ_1:def 3;

        then

        reconsider Wf as Element of ((n + k) -tuples_on {A, B}) by A34, FINSEQ_2: 92;

        Wf is A, n, B, k -dominated-election

        proof

          

           A39: 0 in ( dom W) by A5, TARSKI:def 2;

          

           A40: 1 in ( dom W) by A5, TARSKI:def 2;

          ( Coim (Wf,A)) = ( Coim (f, 0 )) by A39, Th7, A15, A18;

          then ( card ( Coim (Wf,A))) = n by A33, Def1;

          hence Wf in ( Election (A,n,B,k)) by Def1;

          let i such that

           A41: i > 0 ;

          

           A42: (Wf | i) = (W * (f | i)) by RELAT_1: 83;

          then

           A43: ( Coim ((Wf | i),A)) = ( Coim ((f | i), 0 )) by A39, Th7, A15, A18;

          

           A44: ( Coim ((Wf | i),B)) = ( Coim ((f | i),1)) by A42, A40, Th7, A15, A19;

          f is 0 , n, 1, k -dominated-election by A33, Def3;

          hence thesis by A41, A43, A44;

        end;

        then

         A45: Wf in ( DominatedElection (A,n,B,k)) by Def3;

        then

         A46: Wf in ( dom C) by FUNCT_2:def 1, A33;

        (C . Wf) = (T * Wf) by A45, A32

        .= ((W " ) * (W * f)) by A6, A7, A1, NECKLACE: 10

        .= (((W " ) * W) * f) by RELAT_1: 36

        .= (( id { 0 , 1}) * f) by A15, A5, FUNCT_1: 39

        .= f by RELAT_1: 53, A36;

        hence thesis by A46, FUNCT_1:def 3;

      end;

      then

       A47: ( DominatedElection ( 0 ,n,1,k)) = ( rng C);

      per cases ;

        suppose

         A48: ( DominatedElection ( 0 ,n,1,k)) = {} ;

        ( DominatedElection (A,n,B,k)) = {}

        proof

          assume ( DominatedElection (A,n,B,k)) <> {} ;

          then

          consider x be object such that

           A49: x in ( DominatedElection (A,n,B,k)) by XBOOLE_0:def 1;

          ex y be object st y in ( DominatedElection ( 0 ,n,1,k)) & P[x, y] by A20, A49;

          hence thesis by A48;

        end;

        hence thesis by A48;

      end;

        suppose ( DominatedElection ( 0 ,n,1,k)) <> {} ;

        then

         A50: ( dom C) = ( DominatedElection (A,n,B,k)) by FUNCT_2:def 1;

        C is one-to-one

        proof

          let x1,x2 be object such that

           A51: x1 in ( dom C) and

           A52: x2 in ( dom C) and

           A53: (C . x1) = (C . x2);

          

           A54: x1 in ( Election (A,n,B,k)) by A50, A51;

          x2 in ( Election (A,n,B,k)) by A50, A52;

          then

          reconsider x1, x2 as Element of ((n + k) -tuples_on {A, B}) by A54;

          

           A55: ( len x1) = (n + k) by CARD_1:def 7;

          

           A56: ( len x2) = (n + k) by CARD_1:def 7;

          

           A57: ( dom x1) = ( Seg (n + k)) by A55, FINSEQ_1:def 3;

          

           A58: ( dom x2) = ( Seg (n + k)) by A56, FINSEQ_1:def 3;

          

           A59: ( rng x1) c= ( dom T) by A2;

          

           A60: ( rng x2) c= ( dom T) by A2;

          

           A61: T is one-to-one by A12, FUNCT_4:def 4;

          

           A62: (C . x1) = (T * x1) by A51, A32;

          (C . x2) = (T * x2) by A52, A32;

          hence thesis by A62, A57, A58, A59, A60, A61, A53, FUNCT_1: 27;

        end;

        hence thesis by WELLORD2:def 4, A47, A50, CARD_1: 5;

      end;

    end;

    theorem :: BALLOT_1:22

    

     Th22: for p be FinSequence of NAT holds p is 0 , n, 1, k -dominated-election iff p is Tuple of (n + k), { 0 , 1} & n > 0 & ( Sum p) = k & for i st i > 0 holds (2 * ( Sum (p | i))) < i

    proof

      let p be FinSequence of NAT ;

      thus p is 0 , n, 1, k -dominated-election implies p is Tuple of (n + k), { 0 , 1} & n > 0 & ( Sum p) = k & for i st i > 0 holds (2 * ( Sum (p | i))) < i

      proof

        assume

         A1: p is 0 , n, 1, k -dominated-election;

        then

        reconsider P = p as Element of ((n + k) -tuples_on { 0 , 1});

        

         A2: ( rng P) c= { 0 , 1};

        then ( Sum p) = (1 * ( card (p " {1}))) by Th21;

        hence p is Tuple of (n + k), { 0 , 1} & n > 0 & ( Sum p) = k by A2, A1, Th11, Th14;

        let i such that

         A3: i > 0 ;

        ( rng (p | i)) c= ( rng p) by RELAT_1: 70;

        then

         A4: ( rng (p | i)) c= { 0 , 1} by A2;

        then

         A5: (1 * ( card ((p | i) " {1}))) = ( Sum (p | i)) by Th21;

        (( card ((p | i) " {1})) + ( card ((p | i) " { 0 }))) = ( len (p | i)) by A4, Th6;

        then (( len (p | i)) - ( Sum (p | i))) > ( Sum (p | i)) by A1, A3, A5;

        then

         A6: ( len (p | i)) > (( Sum (p | i)) + ( Sum (p | i))) by XREAL_1: 20;

        per cases ;

          suppose

           A7: i > ( len p);

          then (p | i) = p by FINSEQ_1: 58;

          hence thesis by A6, A7, XXREAL_0: 2;

        end;

          suppose i <= ( len p);

          hence thesis by FINSEQ_1: 59, A6;

        end;

      end;

      assume that

       A8: p is Tuple of (n + k), { 0 , 1} and

       A9: n > 0 and

       A10: ( Sum p) = k and

       A11: for i st i > 0 holds (2 * ( Sum (p | i))) < i;

      

       A12: ( rng p) c= { 0 , 1} by A8, FINSEQ_1:def 4;

      

       A13: ( len p) = (n + k) by A8, CARD_1:def 7;

      

       A14: (1 * ( card (p " {1}))) = k by A12, Th21, A10;

      reconsider P = p as Element of ((n + k) -tuples_on { 0 , 1}) by A8, FINSEQ_2: 92, A13;

      

       A15: (( card (p " {1})) + ( card (p " { 0 }))) = ( len p) by A12, Th6;

      then ( card (P " { 0 })) = n by A14, A13;

      hence p in ( Election ( 0 ,n,1,k)) by Def1;

      let i such that

       A16: i > 0 ;

      ( rng (p | i)) c= ( rng p) by RELAT_1: 70;

      then

       A17: ( rng (p | i)) c= { 0 , 1} by A12;

      then

       A18: (1 * ( card ((p | i) " {1}))) = ( Sum (p | i)) by Th21;

      

       A19: (2 * ( Sum (p | i))) < i by A16, A11;

      

       A20: (( card ((p | i) " {1})) + ( card ((p | i) " { 0 }))) = ( len (p | i)) by A17, Th6;

      per cases ;

        suppose i > ( len p);

        then

         A21: (p | i) = p by FINSEQ_1: 58;

        (p | ( len p)) = p by FINSEQ_1: 58;

        then (2 * ( Sum p)) < ( len p) by A8, A9, A11;

        then (k + k) < (n + k) by A8, A10, CARD_1:def 7;

        hence thesis by XREAL_1: 6, A14, A15, A13, A21;

      end;

        suppose i <= ( len p);

        then (( card ((p | i) " {1})) + ( card ((p | i) " {1}))) < (( card ((p | i) " {1})) + ( card ((p | i) " { 0 }))) by FINSEQ_1: 59, A18, A20, A19;

        hence thesis by XREAL_1: 6;

      end;

    end;

    theorem :: BALLOT_1:23

    

     Th23: f is A, n, B, k -dominated-election implies (f . 1) = A

    proof

      set f1 = (f | 1);

      assume

       A1: f is A, n, B, k -dominated-election;

      then n > k by Th14;

      then ( len f) >= (1 + 0 ) by A1, NAT_1: 13;

      then

       A2: ( len f1) = 1 by FINSEQ_1: 59;

      ( card (f1 " {A})) > ( card (f1 " {B})) by A1;

      then

       A3: (f1 " {A}) is non empty;

      ( dom f1) = ( Seg 1) by FINSEQ_1:def 3, A2;

      then

       A4: (f1 " {A}) = {1} by RELAT_1: 132, FINSEQ_1: 2, A3, ZFMISC_1: 33;

      1 in {1} by FINSEQ_1: 2;

      then (f1 . 1) in {A} by A4, FUNCT_1:def 7;

      then A = (f1 . 1) by TARSKI:def 1;

      hence thesis by FINSEQ_3: 112;

    end;

    theorem :: BALLOT_1:24

    

     Th24: for d be XFinSequence of NAT holds d in ( Domin_0 ((n + k),k)) iff ( <* 0 *> ^ ( XFS2FS d)) in ( DominatedElection ( 0 ,(n + 1),1,k))

    proof

      let d be XFinSequence of NAT ;

      set Xd = ( XFS2FS d), Z = <* 0 *>, ZXd = (Z ^ Xd);

      ( rng d) c= REAL ;

      then

      reconsider D = d as XFinSequence of REAL by RELAT_1:def 19;

      

       A1: ( len Z) = 1 by FINSEQ_1: 39;

      ( rng Z) = { 0 } by FINSEQ_1: 39;

      then

       A2: ( rng Z) c= { 0 , 1} by ZFMISC_1: 7;

      

       A3: ( XFS2FS d) = ( XFS2FS D) by Th3;

      thus d in ( Domin_0 ((n + k),k)) implies ZXd in ( DominatedElection ( 0 ,(n + 1),1,k))

      proof

        assume

         A4: d in ( Domin_0 ((n + k),k));

        then

         A5: d is dominated_by_0 by CATALAN2: 20;

        

         A6: ( Sum d) = k by A4, CATALAN2: 20;

        ( len d) = (n + k) by A4, CATALAN2: 20;

        then

         A7: ( len Xd) = (n + k) by AFINSQ_1:def 9;

        

         A8: ( rng Xd) c= { 0 , 1} by A5, Th2;

        ( rng (Z ^ Xd)) = (( rng Z) \/ ( rng Xd)) by FINSEQ_1: 31;

        then

        reconsider ZX = ZXd as FinSequence of { 0 , 1} by XBOOLE_1: 8, A8, A2, FINSEQ_1:def 4;

        ( len ZX) = ((n + k) + 1) by A1, A7, FINSEQ_1: 22;

        then

         A9: ZX is Tuple of ((n + 1) + k), { 0 , 1} by CARD_1:def 7;

        

         A10: ( Sum ZXd) = ( 0 + ( Sum Xd)) by RVSUM_1: 76

        .= ( 0 + ( addreal $$ ( XFS2FS D))) by RVSUM_1:def 12, A3

        .= ( addreal "**" D) by AFINSQ_2: 44

        .= k by A6, AFINSQ_2: 48;

        for i st i > 0 holds (2 * ( Sum (ZXd | i))) < i

        proof

          let i such that

           A11: i > 0 ;

          reconsider i1 = (i - 1) as Nat by A11, NAT_1: 14, NAT_1: 21;

          (ZXd | i) = (ZXd | ( Seg (i1 + 1)))

          .= (Z ^ (Xd | i1)) by A1, FINSEQ_6: 14;

          

          then

           A12: ( Sum (ZXd | i)) = ( 0 + ( Sum (Xd | i1))) by RVSUM_1: 76

          .= ( 0 + ( Sum ( XFS2FS (d | i1)))) by Th1

          .= ( Sum ( XFS2FS (D | i1))) by Th3

          .= ( addreal $$ ( XFS2FS (D | i1))) by RVSUM_1:def 12

          .= ( addreal "**" (D | i1)) by AFINSQ_2: 44

          .= ( Sum (d | i1)) by AFINSQ_2: 48;

          (2 * ( Sum (d | i1))) < (i1 + 1) by A5, CATALAN2: 2, NAT_1: 13;

          hence thesis by A12;

        end;

        then ZXd is 0 , (n + 1), 1, k -dominated-election by A9, Th22, A10;

        hence thesis by Def3;

      end;

      assume ZXd in ( DominatedElection ( 0 ,(n + 1),1,k));

      then

       A13: ZXd is 0 , (n + 1), 1, k -dominated-election by Def3;

      then ZXd is Tuple of ((n + 1) + k), { 0 , 1} by Th22;

      then

       A14: ( rng ZXd) c= { 0 , 1} by FINSEQ_1:def 4;

      ( rng Xd) c= ( rng ZXd) by FINSEQ_1: 30;

      then

       A15: ( rng Xd) c= { 0 , 1} by A14;

      

       A16: ( len ZXd) = ((n + 1) + k) by A13, CARD_1:def 7;

      

       A17: ( len ZXd) = (1 + ( len Xd)) by A1, FINSEQ_1: 22;

      

       A18: ( len Xd) = ( len d) by AFINSQ_1:def 9;

      for k st k <= ( dom d) holds (2 * ( Sum (d | k))) <= k

      proof

        let k such that k <= ( dom d);

        (ZXd | (k + 1)) = (Z ^ (Xd | k)) by A1, FINSEQ_6: 14;

        

        then ( Sum (ZXd | (k + 1))) = ( 0 + ( Sum (Xd | k))) by RVSUM_1: 76

        .= ( 0 + ( Sum ( XFS2FS (d | k)))) by Th1

        .= ( Sum ( XFS2FS (D | k))) by Th3

        .= ( addreal $$ ( XFS2FS (D | k))) by RVSUM_1:def 12

        .= ( addreal "**" (D | k)) by AFINSQ_2: 44

        .= ( Sum (d | k)) by AFINSQ_2: 48;

        then (2 * ( Sum (d | k))) < (k + 1) by A13, Th22;

        hence thesis by NAT_1: 13;

      end;

      then

       A19: d is dominated_by_0 by A15, Th2;

      ( Sum ZXd) = ( 0 + ( Sum Xd)) by RVSUM_1: 76

      .= ( Sum ( XFS2FS D)) by Th3

      .= ( addreal $$ ( XFS2FS D)) by RVSUM_1:def 12

      .= ( addreal "**" D) by AFINSQ_2: 44

      .= ( Sum d) by AFINSQ_2: 48;

      then ( Sum d) = k by A13, Th22;

      hence d in ( Domin_0 ((n + k),k)) by A19, A16, A17, A18, CATALAN2:def 2;

    end;

    theorem :: BALLOT_1:25

    ( card ( Domin_0 ((n + k),k))) = ( card ( DominatedElection ( 0 ,(n + 1),1,k)))

    proof

      set D = ( Domin_0 ((n + k),k)), B = ( DominatedElection ( 0 ,(n + 1),1,k));

      set Z = <* 0 *>;

      defpred F[ object, object] means for d be XFinSequence of NAT st d = $1 holds $2 = (Z ^ ( XFS2FS d));

      

       A1: for x be object st x in D holds ex y be object st y in B & F[x, y]

      proof

        let x be object;

        assume

         A2: x in D;

        then

        consider p be XFinSequence of NAT such that

         A3: p = x and p is dominated_by_0 & ( dom p) = (n + k) & ( Sum p) = k by CATALAN2:def 2;

        take y = (Z ^ ( XFS2FS p));

        thus thesis by Th24, A3, A2;

      end;

      consider f be Function of D, B such that

       A4: for x be object st x in D holds F[x, (f . x)] from FUNCT_2:sch 1( A1);

      per cases ;

        suppose B <> {} ;

        then

         A5: ( dom f) = D by FUNCT_2:def 1;

        B c= ( rng f)

        proof

          let y be object;

          assume

           A6: y in B;

          then y in ( Election ( 0 ,(n + 1),1,k));

          then

          reconsider g = y as Element of (((n + 1) + k) -tuples_on { 0 , 1});

          g is 0 , (n + 1), 1, k -dominated-election by A6, Def3;

          then

           A7: (g . 1) = 0 by Th23;

          consider d be Element of { 0 , 1}, dg be FinSequence of { 0 , 1} such that

           A8: d = (g . 1) and

           A9: g = ( <*d*> ^ dg) by FINSEQ_3: 102;

           { 0 , 1} c= NAT ;

          then ( rng ( FS2XFS dg)) c= NAT ;

          then

          reconsider G = ( FS2XFS dg) as XFinSequence of NAT by RELAT_1:def 19;

          ( XFS2FS G) = ( XFS2FS ( FS2XFS dg)) by Th3;

          then

           A10: ( XFS2FS G) = dg;

          then

           A11: G in D by A6, A8, A9, A7, Th24;

          (f . G) = g by A10, A6, A8, A9, A7, Th24, A4;

          hence thesis by A11, A5, FUNCT_1:def 3;

        end;

        then

         A12: ( rng f) = B;

        f is one-to-one

        proof

          let x1,x2 be object such that

           A13: x1 in ( dom f) and

           A14: x2 in ( dom f) and

           A15: (f . x1) = (f . x2);

          consider p1 be XFinSequence of NAT such that

           A16: p1 = x1 and p1 is dominated_by_0 & ( dom p1) = (n + k) & ( Sum p1) = k by A13, CATALAN2:def 2;

          consider p2 be XFinSequence of NAT such that

           A17: p2 = x2 and p2 is dominated_by_0 & ( dom p2) = (n + k) & ( Sum p2) = k by A14, CATALAN2:def 2;

          

           A18: (f . p1) = (Z ^ ( XFS2FS p1)) by A16, A13, A4;

          (f . p2) = (Z ^ ( XFS2FS p2)) by A14, A17, A4;

          then ( XFS2FS p1) = ( XFS2FS p2) by A18, A15, A16, A17, FINSEQ_1: 33;

          hence thesis by Th4, A16, A17;

        end;

        hence thesis by WELLORD2:def 4, A5, A12, CARD_1: 5;

      end;

        suppose

         A19: B = {} ;

        D = {}

        proof

          assume D <> {} ;

          then

          consider x be object such that

           A20: x in D by XBOOLE_0:def 1;

          ex y be object st y in B & F[x, y] by A20, A1;

          hence thesis by A19;

        end;

        hence thesis by A19;

      end;

    end;

    theorem :: BALLOT_1:26

    

     Th26: ( card ( Domin_0 ((n + k),k))) = ( card ( DominatedElection ( 0 ,(n + 1),1,k)))

    proof

      set D = ( Domin_0 ((n + k),k)), B = ( DominatedElection ( 0 ,(n + 1),1,k));

      set Z = <* 0 *>;

      defpred F[ object, object] means for d be XFinSequence of NAT st d = $1 holds $2 = (Z ^ ( XFS2FS d));

      

       A1: for x be object st x in D holds ex y be object st y in B & F[x, y]

      proof

        let x be object;

        assume

         A2: x in D;

        then

        consider p be XFinSequence of NAT such that

         A3: p = x and p is dominated_by_0 & ( dom p) = (n + k) & ( Sum p) = k by CATALAN2:def 2;

        take y = (Z ^ ( XFS2FS p));

        thus thesis by Th24, A3, A2;

      end;

      consider f be Function of D, B such that

       A4: for x be object st x in D holds F[x, (f . x)] from FUNCT_2:sch 1( A1);

      per cases ;

        suppose B <> {} ;

        then

         A5: ( dom f) = D by FUNCT_2:def 1;

        B c= ( rng f)

        proof

          let y be object;

          assume

           A6: y in B;

          then y in ( Election ( 0 ,(n + 1),1,k));

          then

          reconsider g = y as Element of (((n + 1) + k) -tuples_on { 0 , 1});

          g is 0 , (n + 1), 1, k -dominated-election by A6, Def3;

          then

           A7: (g . 1) = 0 by Th23;

          consider d be Element of { 0 , 1}, dg be FinSequence of { 0 , 1} such that

           A8: d = (g . 1) and

           A9: g = ( <*d*> ^ dg) by FINSEQ_3: 102;

           { 0 , 1} c= NAT ;

          then ( rng ( FS2XFS dg)) c= NAT ;

          then

          reconsider G = ( FS2XFS dg) as XFinSequence of NAT by RELAT_1:def 19;

          ( XFS2FS G) = ( XFS2FS ( FS2XFS dg)) by Th3;

          then

           A10: ( XFS2FS G) = dg;

          then

           A11: G in D by A6, A8, A9, A7, Th24;

          (f . G) = g by A10, A6, A8, A9, A7, Th24, A4;

          hence thesis by A11, A5, FUNCT_1:def 3;

        end;

        then

         A12: ( rng f) = B;

        f is one-to-one

        proof

          let x1,x2 be object such that

           A13: x1 in ( dom f) and

           A14: x2 in ( dom f) and

           A15: (f . x1) = (f . x2);

          consider p1 be XFinSequence of NAT such that

           A16: p1 = x1 and p1 is dominated_by_0 & ( dom p1) = (n + k) & ( Sum p1) = k by A13, CATALAN2:def 2;

          consider p2 be XFinSequence of NAT such that

           A17: p2 = x2 and p2 is dominated_by_0 & ( dom p2) = (n + k) & ( Sum p2) = k by A14, CATALAN2:def 2;

          

           A18: (f . p1) = (Z ^ ( XFS2FS p1)) by A16, A13, A4;

          (f . p2) = (Z ^ ( XFS2FS p2)) by A14, A17, A4;

          then ( XFS2FS p1) = ( XFS2FS p2) by A18, A15, A16, A17, FINSEQ_1: 33;

          hence thesis by Th4, A16, A17;

        end;

        hence thesis by WELLORD2:def 4, A5, A12, CARD_1: 5;

      end;

        suppose

         A19: B = {} ;

        D = {}

        proof

          assume D <> {} ;

          then

          consider x be object such that

           A20: x in D by XBOOLE_0:def 1;

          ex y be object st y in B & F[x, y] by A20, A1;

          hence thesis by A19;

        end;

        hence thesis by A19;

      end;

    end;

    theorem :: BALLOT_1:27

    

     Th27: A <> B & n > k implies ( card ( DominatedElection (A,n,B,k))) = (((n - k) / (n + k)) * ((n + k) choose k))

    proof

      assume that

       A1: A <> B and

       A2: n > k;

      reconsider n1 = (n - 1) as Nat by A2, NAT_1: 20;

      

       A3: (n1 + 1) = n;

      then n1 >= k by A2, NAT_1: 13;

      then

       A4: (n1 + k) >= (k + k) by XREAL_1: 6;

      

       A5: (n1 + k) >= (k + 0 ) by XREAL_1: 6;

      

       A6: (n + k) >= (k + 0 ) by XREAL_1: 6;

      set n1k = (n1 + k), nk = (n + k);

      

       A7: (n1k + 1) = nk;

      (n * (1 / n)) = 1 by A2, XCMPLX_1: 106;

      

      then

       A8: ((nk ! ) / ((n1 ! ) * (k ! ))) = ((n * (1 / n)) * ((nk ! ) / ((n1 ! ) * (k ! ))))

      .= (n * ((1 / n) * ((nk ! ) / ((n1 ! ) * (k ! )))))

      .= (n * ((nk ! ) / (n * ((n1 ! ) * (k ! ))))) by XCMPLX_1: 103

      .= (n * ((nk ! ) / ((n * (n1 ! )) * (k ! ))))

      .= (n * ((nk ! ) / ((n ! ) * (k ! )))) by A3, NEWTON: 15;

      (nk * (1 / nk)) = 1 by A2, XCMPLX_1: 106;

      

      then

       A9: ((n1k ! ) / ((n1 ! ) * (k ! ))) = ((nk * (1 / nk)) * ((n1k ! ) / ((n1 ! ) * (k ! ))))

      .= ((1 / nk) * (nk * ((n1k ! ) / ((n1 ! ) * (k ! )))))

      .= ((1 / nk) * ((nk * (n1k ! )) / ((n1 ! ) * (k ! )))) by XCMPLX_1: 74

      .= ((1 / nk) * ((nk ! ) / ((n1 ! ) * (k ! )))) by A7, NEWTON: 15

      .= (((1 / nk) * n) * ((nk ! ) / ((n ! ) * (k ! )))) by A8

      .= ((n / nk) * ((nk ! ) / ((n ! ) * (k ! )))) by XCMPLX_1: 99;

      

       A10: ((n1 + k) - k) = n1;

      

       A11: (nk - k) = n;

      

      thus ( card ( DominatedElection (A,n,B,k))) = ( card ( DominatedElection ( 0 ,(n1 + 1),1,k))) by A1, Th20

      .= ( card ( Domin_0 ((n1 + k),k))) by Th26

      .= (((((n1 + k) + 1) - (2 * k)) / (((n1 + k) + 1) - k)) * ((n1 + k) choose k)) by A4, CATALAN2: 29

      .= (((n - k) / n) * ((n1k ! ) / ((n1 ! ) * (k ! )))) by NEWTON:def 3, A5, A10

      .= ((((n - k) / n) * (n / nk)) * ((nk ! ) / ((n ! ) * (k ! )))) by A9

      .= (((n - k) / nk) * ((nk ! ) / ((n ! ) * (k ! )))) by A2, XCMPLX_1: 98

      .= (((n - k) / nk) * (nk choose k)) by A11, A6, NEWTON:def 3;

    end;

    begin

    ::$Notion-Name

    theorem :: BALLOT_1:28

    A <> B & n >= k implies ( prob ( DominatedElection (A,n,B,k))) = ((n - k) / (n + k))

    proof

      assume

       A1: A <> B & n >= k;

      then

       A2: ( card ( Election (A,n,B,k))) = ((n + k) choose n) by Th12;

      

       A3: (n + k) >= (k + 0 ) & ((n + k) - k) = n & (n + k) >= n by NAT_1: 11;

      

       A4: ((n + k) choose n) > 0 by NAT_1: 11, CATALAN2: 26;

      per cases by A1, XXREAL_0: 1;

        suppose

         A5: n = k;

        then ( DominatedElection (A,n,B,k)) is empty by Th18;

        then ( card ( DominatedElection (A,n,B,k))) = 0 ;

        then ( prob ( DominatedElection (A,n,B,k))) = ( 0 / ((n + k) choose n)) by A2, RPR_1:def 1;

        hence thesis by A5;

      end;

        suppose n > k;

        

        then

         A6: ( card ( DominatedElection (A,n,B,k))) = (((n - k) / (n + k)) * ((n + k) choose k)) by A1, Th27

        .= (((n - k) / (n + k)) * ((n + k) choose n)) by A3, NEWTON: 20;

        

        thus ( prob ( DominatedElection (A,n,B,k))) = ((((n - k) / (n + k)) * ((n + k) choose n)) / ((n + k) choose n)) by A2, A6, RPR_1:def 1

        .= (((n - k) / (n + k)) * (((n + k) choose n) / ((n + k) choose n))) by XCMPLX_1: 74

        .= (((n - k) / (n + k)) * 1) by A4, XCMPLX_1: 60

        .= ((n - k) / (n + k));

      end;

    end;