---

Step * of Lemma assert-rcvd-inning-eq

∀[V:Type]
  ∀A:Id List. ∀r:consensus-rcv(V;A). ∀i:ℕ.
    (↑inning(r) =z i ⇐⇒ ∃a:{b:Id| (b ∈ A)} . ∃v:V. (r = Vote[a;i;v] ∈ consensus-rcv(V;A)))
BY
{ (((UnivCD THENA Auto) THEN D -2)
   THEN Try (RepeatFor 2 (D -2))
   THEN RepUR ``rcvd-inning-eq rcv-vote? rcvd-vote`` 0
   THEN Auto
   THEN ExRepD
   THEN All (RW assert_pushdownC)
   THEN Auto) }

1
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

2
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))

3
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 ∈ ℤ

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}r:consensus-rcv(V;A).  \mforall{}i:\mBbbN{}.
        (\muparrow{}inning(r)  =\msubz{}  i  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{b:Id|  (b  \mmember{}  A)\}  .  \mexists{}v:V.  (r  =  Vote[a;i;v]))


By

(((UnivCD  THENA  Auto)  THEN  D  -2)
  THEN  Try  (RepeatFor  2  (D  -2))
  THEN  RepUR  ``rcvd-inning-eq  rcv-vote?  rcvd-vote``  0
  THEN  Auto
  THEN  ExRepD
  THEN  All  (RW  assert\_pushdownC)
  THEN  Auto)

---

Home Index