Nuprl Lemma : member-votes-from-inning
∀[V:Type]
∀A:Id List. ∀L:consensus-rcv(V;A) List. ∀i:ℕ. ∀b:{b:Id| (b ∈ A)} . ∀v:V.
((<b, v> ∈ votes-from-inning(i;L)) ⇐⇒ (Vote[b;i;v] ∈ L))
Proof
Definitions occuring in Statement :
votes-from-inning: votes-from-inning(i;L),
cs-rcv-vote: Vote[a;i;v],
consensus-rcv: consensus-rcv(V;A),
Id: Id,
l_member: (x ∈ l),
list: T List,
nat: ℕ,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
set: {x:A| B[x]} ,
pair: <a, b>,
product: x:A × B[x],
universe: Type
Lemmas :
exists_wf,
consensus-rcv_wf,
l_member_wf,
assert_wf,
rcvd-inning-eq_wf,
Id_wf,
rcvd-vote_wf,
bool_cases_sqequal,
bfalse_wf,
btrue_wf,
nat_wf,
cs-rcv-vote_wf,
member-mapfilter,
mapfilter_wf,
subtype_rel_sum,
iff_wf,
assert_of_eq_int,
squash_wf,
true_wf,
set_wf,
list_wf,
sq_stable__le,
le_wf,
and_wf,
equal_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}L:consensus-rcv(V;A) List. \mforall{}i:\mBbbN{}. \mforall{}b:\{b:Id| (b \mmember{} A)\} . \mforall{}v:V.
((<b, v> \mmember{} votes-from-inning(i;L)) \mLeftarrow{}{}\mRightarrow{} (Vote[b;i;v] \mmember{} L))
Date html generated:
2015_07_17-AM-11_47_59
Last ObjectModification:
2015_01_28-AM-00_46_05
Home
Index