---

Step * 1 of Lemma assert-rcvd-inning-gt


1. V : Type
2. A : Id List@i
3. x : V@i
4. i : ℤ@i
5. a : {b:Id| (b ∈ A)} @i
6. v : V@i
7. j : ℕ@i
8. i < j@i
9. (inl x) = Vote[a;j;v] ∈ consensus-rcv(V;A)@i
⊢ False
BY
{ (RepUR ``cs-rcv-vote consensus-rcv`` -1 THEN Auto) }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List@i
3.  x  :  V@i
4.  i  :  \mBbbZ{}@i
5.  a  :  \{b:Id|  (b  \mmember{}  A)\}  @i
6.  v  :  V@i
7.  j  :  \mBbbN{}@i
8.  i  <  j@i
9.  (inl  x)  =  Vote[a;j;v]@i
\mvdash{}  False


By

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

---

Home Index