---

Step * of Lemma assert-cs-is-considering

∀[V:Type]. ∀x:consensus-state3(V). (↑cs-is-considering(x) ⇐⇒ ∃v:V. (x = CONSIDERING[v] ∈ consensus-state3(V)))
BY
{ (Unfolds ``consensus-state3 cs-is-considering cs-considering`` 0
   THEN Auto
   THEN ExRepD
   THEN DVar `x'
   THEN All Reduce
   THEN Auto) }

1
1. [V] : Type
2. y : V + 𝔹@i
3. ↑isl(y)@i
⊢ ∃v:V. ((inr y ) = (inr (inl v) ) ∈ (V + V + 𝔹))

---

Latex:


\mforall{}[V:Type].  \mforall{}x:consensus-state3(V).  (\muparrow{}cs-is-considering(x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}v:V.  (x  =  CONSIDERING[v]))


By

(Unfolds  ``consensus-state3  cs-is-considering  cs-considering``  0
  THEN  Auto
  THEN  ExRepD
  THEN  DVar  `x'
  THEN  All  Reduce
  THEN  Auto)

---

Home Index