### Nuprl Lemma : assert-rcvd-inning-gt

`∀[V:Type]`
`  ∀A:Id List. ∀r:consensus-rcv(V;A). ∀i:ℤ.`
`    (↑i <z inning(r) `⇐⇒` ∃a:{b:Id| (b ∈ A)} . ∃v:V. ∃j:ℕ. (i < j ∧ (r = Vote[a;j;v] ∈ consensus-rcv(V;A))))`

Proof

Definitions occuring in Statement :  rcvd-inning-gt: `i <z inning(r)` cs-rcv-vote: `Vote[a;i;v]` consensus-rcv: `consensus-rcv(V;A)` Id: `Id` l_member: `(x ∈ l)` list: `T List` nat: `ℕ` assert: `↑b` less_than: `a < b` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  false_wf exists_wf l_member_wf nat_wf less_than_wf subtype_rel_sum cs-rcv-vote_wf assert_of_lt_int assert_wf lt_int_wf assert_witness consensus-rcv_wf list_wf Id_wf btrue_wf and_wf equal_wf isl_wf bfalse_wf btrue_neq_bfalse outr_wf set_wf le_wf less_than_transitivity1 le_weakening
\mforall{}[V:Type]
\mforall{}A:Id  List.  \mforall{}r:consensus-rcv(V;A).  \mforall{}i:\mBbbZ{}.
(\muparrow{}i  <z  inning(r)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{b:Id|  (b  \mmember{}  A)\}  .  \mexists{}v:V.  \mexists{}j:\mBbbN{}.  (i  <  j  \mwedge{}  (r  =  Vote[a;j;v])))

Date html generated: 2015_07_17-AM-11_47_32
Last ObjectModification: 2015_01_28-AM-01_31_17

Home Index