let n, k be Nat; 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 being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )
let p be FinSequence of NAT ; ( p is 0 ,n,1,k -dominated-election iff ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )
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 being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )
( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) implies p is 0 ,n,1,k -dominated-election )proof
assume A1:
p is
0 ,
n,1,
k -dominated-election
;
( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) )
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;
for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i
let i be
Nat;
( i > 0 implies 2 * (Sum (p | i)) < i )
assume A3:
i > 0
;
2 * (Sum (p | i)) < i
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;
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 being Nat st i > 0 holds
2 * (Sum (p | i)) < i
; p is 0 ,n,1,k -dominated-election
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; BALLOT_1:def 2 for i being Nat st i > 0 holds
card ((p | i) " {0}) > card ((p | i) " {1})
let i be Nat; ( i > 0 implies card ((p | i) " {0}) > card ((p | i) " {1}) )
assume A16:
i > 0
; card ((p | i) " {0}) > card ((p | i) " {1})
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;