---

Step * 1 of Lemma consensus-state4-exclusive-cases


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. a : {a:Id| (a ∈ A)} @i
5. i : ℤ@i
6. by state s, a passed inning i without archiving a value
7. by state s, a passed inning i without archiving a value
⊢ ¬in state s, a has not completed inning i
BY
{ ((D 0 THEN Auto) THEN D -2 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  [V]  :  Type
2.  A  :  Id  List@i
3.  s  :  ConsensusState@i
4.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
5.  i  :  \mBbbZ{}@i
6.  by  state  s,  a  passed  inning  i  without  archiving  a  value
7.  by  state  s,  a  passed  inning  i  without  archiving  a  value
\mvdash{}  \mneg{}in  state  s,  a  has  not  completed  inning  i


By

---

Latex:
((D  0  THEN  Auto)  THEN  D  -2  THEN  D  -1  THEN  Auto)

---

Home Index