---

Step * 3 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. a : {b:Id| (b ∈ A)} @i
8. v : V@i
9. (inr <y1, y3, y4> ) = Vote[a;i;v] ∈ consensus-rcv(V;A)@i
⊢ i = y3 ∈ ℤ
BY
{ (RepUR ``cs-rcv-vote consensus-rcv`` -1 THEN RepeatFor 3 (AutoSimpHyp Auto (-1)) 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.  a  :  \{b:Id|  (b  \mmember{}  A)\}  @i
8.  v  :  V@i
9.  (inr  <y1,  y3,  y4>  )  =  Vote[a;i;v]@i
\mvdash{}  i  =  y3


By

(RepUR  ``cs-rcv-vote  consensus-rcv``  -1  THEN  RepeatFor  3  (AutoSimpHyp  Auto  (-1))  THEN  Auto)

---

Home Index