---

Step * of Lemma assert-rcvd-inning-gt

∀[V:Type]
  ∀A:Id List. ∀r:consensus-rcv(V;A). ∀i:ℤ.
    (↑i <z inning(r) ⇐⇒ ∃a:{b:Id| (b ∈ A)} . ∃v:V. ∃j:ℕ. (i < j ∧ (r = Vote[a;j;v] ∈ consensus-rcv(V;A))))
BY
{ (((UnivCD THENA Auto) THEN D -2)
   THEN Try (RepeatFor 2 (D -2))
   THEN RepUR ``rcvd-inning-gt 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. j : ℕ@i
8. i < j@i
9. (inl x) = Vote[a;j;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. a : {b:Id| (b ∈ A)} @i
8. v : V@i
9. j : ℕ@i
10. i < j@i
11. (inr <y1, y3, y4> ) = Vote[a;j;v] ∈ consensus-rcv(V;A)@i
⊢ i < y3

---

Latex:


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


By

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

---

Home Index