---

Step * of Lemma assert-cs-is-decided

∀[V:Type]. ∀x:consensus-state2(V). (↑cs-is-decided(x) ⇐⇒ ∃v:V. (x = Decided[v] ∈ consensus-state2(V)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D -1 THEN RepUR ``cs-is-decided cs-decided consensus-state2`` 0 THEN Auto) }

1
1. V : Type
2. y : V + Top@i
3. ∃v:V. ((inr y ) = (inl v) ∈ (V + V + Top))@i
⊢ False

---

Latex:


\mforall{}[V:Type].  \mforall{}x:consensus-state2(V).  (\muparrow{}cs-is-decided(x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}v:V.  (x  =  Decided[v]))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  RepUR  ``cs-is-decided  cs-decided  consensus-state2``  0
  THEN  Auto)

---

Home Index