Nuprl Lemma : rcvd-vote_wf

[V:Type]. ∀[A:Id List]. ∀[x:consensus-rcv(V;A)].  rcvd-vote(x) ∈ {b:Id| (b ∈ A)}  × ℕ × supposing ↑rcv-vote?(x)


Proof




Definitions occuring in Statement :  rcvd-vote: rcvd-vote(x) rcv-vote?: rcv-vote?(x) consensus-rcv: consensus-rcv(V;A) Id: Id l_member: (x ∈ l) list: List nat: assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  product: x:A × B[x] universe: Type
Lemmas :  false_wf true_wf consensus-rcv_wf list_wf Id_wf assert_wf rcv-vote?_wf
\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[x:consensus-rcv(V;A)].
    rcvd-vote(x)  \mmember{}  \{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  \mBbbN{}  \mtimes{}  V  supposing  \muparrow{}rcv-vote?(x)



Date html generated: 2015_07_17-AM-11_47_19
Last ObjectModification: 2015_01_28-AM-01_29_17

Home Index