---

Step * 1 1 1 of Lemma votes-from-inning-is-nil


1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n < i
8. j : ℕ||L||@i
9. (L[j] ∈ L)
⊢ (↑inning(L[j]) =z i) ⇒ (↑n <z inning(L[j]))
BY
{ (GenConclAtAddr [1;1;2]
   THEN ((D -2 THEN Try (RepeatFor 2 (D -2)))
         THEN RepUR ``rcvd-inning-eq rcvd-inning-gt rcv-vote? rcvd-vote`` 0
         THEN Try ((RW assert_pushdownC 0 THENA Auto))
         THEN Auto)⋅
   )⋅ }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  L  :  consensus-rcv(V;A)  List
4.  i  :  \mBbbZ{}
5.  n  :  \mBbbZ{}
6.  filter(\mlambda{}r.n  <z  inning(r);L)  =  []
7.  n  <  i
8.  j  :  \mBbbN{}||L||@i
9.  (L[j]  \mmember{}  L)
\mvdash{}  (\muparrow{}inning(L[j])  =\msubz{}  i)  {}\mRightarrow{}  (\muparrow{}n  <z  inning(L[j]))


By

(GenConclAtAddr  [1;1;2]
  THEN  ((D  -2  THEN  Try  (RepeatFor  2  (D  -2)))
              THEN  RepUR  ``rcvd-inning-eq  rcvd-inning-gt  rcv-vote?  rcvd-vote``  0
              THEN  Try  ((RW  assert\_pushdownC  0  THENA  Auto))
              THEN  Auto)\mcdot{}
  )\mcdot{}

---

Home Index