---

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


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. (inl x) = Vote[a;i;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  :  \mBbbN{}@i
5.  a  :  \{b:Id|  (b  \mmember{}  A)\}  @i
6.  v  :  V@i
7.  (inl  x)  =  Vote[a;i;v]@i
\mvdash{}  False


By

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

---

Home Index