:: Bertrand's Ballot Theorem :: by Karol P\kak :: :: Received June 13, 2014 :: Copyright (c) 2014-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, FINSEQ_2, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, FUNCOP_1, BINOP_2, REALSET1, FUNCT_4, CARD_FIN, BALLOT_1, RPR_1, REAL_1, PRGCOR_2, CATALAN2, VALUED_0, SETWISEO; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1, FUNCT_1, XCMPLX_0, FINSET_1, XXREAL_0, AFINSQ_1, RELSET_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, FUNCT_2, FUNCT_4, FUNCOP_1, BINOP_2, AFINSQ_2, NEWTON, XREAL_0, RPR_1, CARD_FIN, CATALAN2, VALUED_0, FINSEQOP, SETWOP_2, RVSUM_1, NAT_D; constructors PARTFUN3, BINOM, WELLORD2, SETWISEO, NAT_D, BINOP_2, RELSET_1, AFINSQ_2, RPR_1, CARD_FIN, CATALAN2, FINSEQOP, FINSOP_1, RVSUM_1, NEWTON; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FUNCT_4, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, AFINSQ_1, RELSET_1, VALUED_0, AFINSQ_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, RVSUM_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0, FUNCT_1; equalities FUNCOP_1, RELAT_1, ORDINAL1, FINSEQ_1, FINSEQ_2; expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, CATALAN2; theorems AFINSQ_1, TARSKI, FUNCT_1, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1, NAT_1, FUNCT_2, XCMPLX_1, CARD_2, WELLORD2, ENUMSET1, CARD_1, NEWTON, XREAL_1, FUNCOP_1, FUNCT_4, XXREAL_0, NAT_D, XREAL_0, AFINSQ_2, ORDINAL1, RPR_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, RVSUM_1, FINSEQ_3, FINSEQ_6, NECKLACE, CARD_FIN, CATALAN2; schemes FUNCT_2, NAT_1; begin :: Preliminaries reserve D,D1,D2 for non empty set, d,d1,d2 for XFinSequence of D, n,k,i,j for Nat; theorem Th1: XFS2FS (d|n) = (XFS2FS d) |n proof set di=d|n, Xd = XFS2FS d,Xdi=XFS2FS di; A1:len Xd = len d by AFINSQ_1:def 9; A2:len Xdi = len di by AFINSQ_1:def 9; per cases; suppose A3: n >= len d; then di=d by AFINSQ_1:52; hence thesis by A3,A1,FINSEQ_1:58; end; suppose A4: n <= len d; then A5: len di = n by AFINSQ_1:54; now let k such that A6: 1 <= k and A7: k <= n; k-'1 = k-1 by A6,XREAL_1:48,XREAL_0:def 2; then k-'1+1 = k; then k-'1 < n by A7,NAT_1:13; then A8: card Segm (k-'1) in card Segm n by NAT_1:41; A9: k <= len d by A4,A7,XXREAL_0:2; thus Xdi.k = di.(k-'1) by A6,A7,A5,AFINSQ_1:def 9 .= d.(k-'1) by A8,A4,AFINSQ_1:53 .= Xd.k by A9,A6,AFINSQ_1:def 9 .= (Xd|n).k by A7,FINSEQ_3:112; end; hence thesis by A5,A4,A1,FINSEQ_1:59,A2; end; end; theorem Th2: rng d = rng (XFS2FS d) proof set Xd = XFS2FS d; A1: len Xd = len d by AFINSQ_1:def 9; thus rng d c= rng Xd proof let y be object; assume y in rng d; then consider x be object such that A2: x in dom d and A3: d.x = y by FUNCT_1:def 3; reconsider x as Nat by A2; A4: x+1-'1=x by NAT_D:34; A5: x+1 <= len d by A2,AFINSQ_1:66,NAT_1:13; then A6: d.x = Xd.(x+1) by NAT_1:11,A4,AFINSQ_1:def 9; x+1 in dom Xd by A1,NAT_1:11,A5,FINSEQ_3:25; hence thesis by A6,A3,FUNCT_1:def 3; end; let y be object; assume y in rng Xd; then consider x be object such that A7: x in dom Xd and A8: Xd.x = y by FUNCT_1:def 3; reconsider x as Nat by A7; A9:1<= x by A7,FINSEQ_3:25; A10:x <= len Xd by A7,FINSEQ_3:25; x-1>=1-1 by A7,FINSEQ_3:25,XREAL_1:9; then A11: x-1=x-'1 by XREAL_0:def 2; A12: d.(x-'1) = Xd.x by A9,A10,A1,AFINSQ_1:def 9; x-'1+1 = x by A11; then x-'1 in dom d by A10,A1,NAT_1:13,AFINSQ_1:66; hence y in rng d by A8,A12,FUNCT_1:def 3; end; theorem 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 such that 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 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 Th5: for d be FinSequence of D holds XFS2FS (FS2XFS d) = d proof let d be FinSequence of D; set Xd=FS2XFS d; A1: len d = len Xd by AFINSQ_1:def 8; A2: len Xd = len XFS2FS Xd by AFINSQ_1:def 9; now let i such that A3: 1<= i and A4: i <= len d; reconsider i1=i-1 as Nat by A3,NAT_1:21; A5: i1+1 = i; A6: i-'1 = i1 by XREAL_0:def 2; thus d.i = Xd.i1 by A4,A5,NAT_1:13,AFINSQ_1:def 8 .= (XFS2FS Xd).i by A3,A4,A6,A1,AFINSQ_1:def 9; end; hence thesis by A1,A2; end; theorem 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 Th7: for f,g be Function st f is one-to-one 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 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 :: Properties of Elections 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; 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 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 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,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 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 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 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 :: Properties of Ballot Elections definition let A,n,B,k; let v be FinSequence; 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 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 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 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 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 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; 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 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 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 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) 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 being 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 Th22: for p being 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}) 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 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 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 being object st x in D ex y being 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 being 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 by Th5; 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 being object st y in B & F[x,y] by A20,A1; hence thesis by A19; end; hence thesis by A19; end; end; theorem 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 being object st x in D ex y being 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 being 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 by Th5; 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 being object st y in B & F[x,y] by A20,A1; hence thesis by A19; end; hence thesis by A19; end; end; theorem 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 :: Main Theorem ::\$N Bertrand's Ballot Theorem theorem 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;