---

Step * 2 of Lemma assert-rcvd-inning-eq


1. [V] : Type
2. A : Id List@i
3. y1 : {b:Id| (b ∈ A)} @i
4. y3 : ℕ@i
5. y4 : V@i
6. i : ℕ@i
7. i = y3 ∈ ℤ
⊢ ∃a:{b:Id| (b ∈ A)} . ∃v:V. ((inr <y1, y3, y4> ) = Vote[a;i;v] ∈ consensus-rcv(V;A))
BY
{ (Fold `cs-rcv-vote` 0 THEN InstConcl [⌈y1⌉;⌈y4⌉]⋅ THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  y1  :  \{b:Id|  (b  \mmember{}  A)\}  @i
4.  y3  :  \mBbbN{}@i
5.  y4  :  V@i
6.  i  :  \mBbbN{}@i
7.  i  =  y3
\mvdash{}  \mexists{}a:\{b:Id|  (b  \mmember{}  A)\}  .  \mexists{}v:V.  ((inr  <y1,  y3,  y4>  )  =  Vote[a;i;v])


By

(Fold  `cs-rcv-vote`  0  THEN  InstConcl  [\mkleeneopen{}y1\mkleeneclose{};\mkleeneopen{}y4\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index